Another way to present MK (which of course prove the consistency of ZF) is the following:
Define: set(x) <-> Exist y. x e y
Axioms: ID axioms +
(1) Unique Construction: if P is a formula in which y occur free but x do not, then all closures of (Exist! x. for all y. y e x <-> set(y) & P) are axioms.
(2) Size: Accessible(x) -> set(x)
Where Accessible(x) is defined as:
Accessible(x) <-> (Exist maximally two m. m e x) OR ~ Exist y: y subset of x & y is uncountable & y is a limit cardinal & y is not reachable by union.
Def.) y is a limit cardinal <-> (for all y. y < x -> Exist z. y < z < x) Def.) y is reachable by union <-> (Exist y. y < x & U(y) =< x)
The relation < is "strict subnumerousity" defined in the usual manner. The relation =< is subnumerousity defined in the usual manner. "subset of" and "uncountable" also defined in the usual manner. "Exist maximally two m. phi(m)" is defined as Exist m,n for all y. phi(y) -> y=m or y=n /
So simply MK is about unique construction of accessible sets, and proper classes of those.