[EDIT] The older exposition of this theory was proved inconsistent by EmilJeřábek (see comments). Here, this is a possible salvage. (the new information over the older post shall be put in square brackets)
Working in mono-sorted FOL with equality and membership, add the following axioms:
Define: $set(y) \iff \exists z: y \in z$
If formula $\phi$ does not use $``x"$, then:
- Comprehension: $(\exists! x \ \forall y \ (y \in x \leftrightarrow set(y) \land \phi))$
Define: $x=V \iff \forall y: set(y) \to y \in x$
- Reflection: $(\phi \to \exists \text { transitive } x \in V: \phi^x)$;
Where $\phi$ is a formula that does not use $``x"$ [having all of its quantifiers bounded by $V$], $\phi^x$ is the formula obtained by merely replacing all bounding occurrences of $V$ in $\phi$ by $x$; "transitive" is defined as a class whose elements are subsets of it.
- Subsetting: $ x \in V \land \forall y \in A (y \subseteq x) \to A \in V$
- Global Choice: For every nonempty class $X$ of pairwise disjoint sets, there is a class having singleton intersection with each nonempty element of $X$.
- Foundation: $\exists y \,(y \in X) \to \exists y \in X \, (y \cap X = \emptyset)$
So the question is:
Is the above theory consistent? Is it equivalent to $\small \sf MK$?