Would the following system succeed in constituting a re-formulation of MK?
Language: mono-sorted first order logic with equality $``="$ and membership $``\in"$, with the following axioms added:
Classes: $\forall \vec{W} \exists! X : X=\{y| \, \phi \land \exists Z (y \in Z) \} $
Let $``V"$ represent the class of all elements.
Let $``ON"$ be the class of all ordinals in $V$.
Define: $R \ is \ ranking \iff \\ R: V \to ON \land \forall x \in V: \\ R(x)= \min \ \{\alpha|\, \forall y \in x : \alpha > R(y)\}$
Sets: $X \in V \iff \exists \ ranking \ R : \{R(y) | \, y \in X\} \not \approx V$
$ \approx $ denotes equinumerousity, i.e. existence of a bijection.
Infinity: $\exists x \in V: x \neq \emptyset \land \forall a\in x\,\exists b\in x: b\supsetneq a$
It is equivalent to MK!
Proof:
That this system proves all axioms of MK.
1-Extensionality is proved simply by letting $\phi$ be $x \in W$ and set $\vec{W}$ to a single parameter $W$, then substitue in class comprehension, and every class would have a unique class that is co-extensional with it.
2- Empty set is proved from infinity and Sets, and so is Pairing.
3- Global choice is enacted by proving $V \approx ON$, since the class of all ranks of elements of $V$ which is $ON$ must be equinumerous with $V$, otherwise it'll be a set and Buralit-Forti would issue.
4- Now we set to prove that the class of all ranks of elements of a class is subnumerouse to that class: we note that any equivalence class of all elements of a class under equivalence relation "having the same rank" would be a set! The reason is because the class of all ranks of its elements is singleton. Now for each class $X$ we take the class of all sets that are equivalence classes of elements of $X$ under equivalence relation "having the same rank", call this class as $P^r(X)$, and clearly this class would be equinumerous to the class of all ranks of elements of $X$. Now since we have global choice, then it is easy to define an injection from $P^r(X)$ to $X$ using any global choice function.
5- Replacement is proved from 4 and axiom of sets straightforwardly, and Separation follows.
6- axiom of Power set is proved for every finite set from axiom of infinity and sets, and if a set is infinite then since we have choice then it is Dedekind infinite, and so the set of all ranks of elements of that set would be equinumerous to the set of all ranks of elements of its power class, and so the power class of it is a set (axiom of sets).
7- axiom of set union is provable since for any set the class of all ranks of elements of its class union is subnumerous to its rank. And also set union is provable from the rest of axioms.
8- Foundation is provable, from infinity which proves existence of a set, and from axiom of sets there must be a ranking function on $V$, so the membership relation on every set must be well founded, otherwise we'll breach the ranking function.
That MK proves all of the above axioms is ovbious, we only need to verify the second axiom, the left to right direction follows from foundation, and the set of ranks of elements of a set being subnumerous to the set which is provable in MK. The opposite direction is provable because any class of stages of the cumulative hierarchy that is smaller than $V$ would be a set, therefore its class union is a set, and so any subclass of that union is a set, since the right hand of the biconditional is equivalent to saying that $X$ is a subclass of a class union of a class of stages that is strictly smaller than $V$, then its provably a set in MK.