I've come across several references to MK (Morse-Kelley set theory), which includes the idea of a proper class, a limitation of size, includes the axiom schema of comprehension across class variables (so for any $\phi(x,\overline y)$ with $x$ restricted to sets, there a class $X=(x : \phi(x,\overline y))$).
I have seen various statements about MK and how it proves the consistency of various things, including $Con(ZF)$, $Con(ZFC)$, $Con(NBG)$, and in fact, for any $T\subset MK$ finitely axiomatized, it proves $Con(T)$.
However, and quite frustratingly, I don't see any references to back up these claims, except occasionally links to other places where the claim was made, but not proven (or even proof-sketched). I would really appreciate a reference where I can see a proof of these claims, or (if it's easier) a quick sketch of why it should be true.
It's not obvious to me at all why quantifying across proper classes should allow this sort of thing, since all relevant sets (sets of proofs, or sets of statements, or whatever) should be contained in some subset of $\omega$, so should be able to be constructed in $ZF$.