[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$?

anyformula, then the schema is obviously inconsistent: e.g., let $\phi$ be $\forall y\,\forall z\,(y\in z\to\exists v\in V\,v=y)$, in which case reflection gives $\exists x\in V\,\forall y\,\forall z\,(y\in z\to\exists v\in x\,v=y)$, i.e., "there is a universal set”. $\endgroup$7more comments