[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:


1. **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$


2. **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.


3. **Subsetting:** $ x \in V \land \forall y \in A (y \subseteq x) \to A \in V$
4. **Global Choice:** For every nonempty class $X$ of pairwise disjoint sets, there is a class having singleton intersection with each nonempty element of $X$.
5. **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$](https://en.wikipedia.org/wiki/Morse%E2%80%93Kelley_set_theory)?
> 
> 
> 



Is this theory equivalent to MK?
This theory is consistent since NBG proves this form of reflection and the rest of axioms are either axioms or theorems of MK, so this theory is a subtheory of MK. Now to establish the other direction of equivalence with MK, we note that Extensionality, Pairing, Boolean union, Set Union, Power, Infinity and Separation all are easily provable using reflection, subsetting, and comprehension, what needs to be proved is Kelley's axiom of [Substitution](https://en.wikipedia.org/wiki/Morse%E2%80%93Kelley_set_theory#The_axioms_in_Kelley%27s_General_Topology).


Now let $F$ be a class function, whose domain is the set $d$, then reflect on the formula $\exists k \in V: k=d \land \forall m \in V (m \in k \to \exists y \in V: y=F(m))$, obviousely from parameters $F,d$; and we get the range of $F$ being a subclass of some transitive set, and by separation it would be a set, thus proving Substitution.


