Working in *mono-sorted* first order logic with equality $``="$ and membership $``\in"$:

*Define:*$set(x) \equiv_{df} \exists y \, (x \in y)$Axiomatize:

**Extensionality:**$( a \subseteq b \land b \subseteq a \to a=b)$**Separation:**$(set(a) \to \exists \ set \ x : \forall y \, (y \in x \leftrightarrow y \in a \land \phi ))$**Reflection:**$ (\varphi \to \exists \ set \ x : \text { trs}(x) \land \varphi^x)$

where formulas $\phi, \varphi$ do not use $``x"$; $\varphi$ do not use $``="$; $\varphi^x$ is obtained from $\varphi$ by merely bounding all of its quantifiers by $``\subseteq x"$; and $``\text { trs}" $ stands for *is transitive*.

This theory can prove: Set existence, Empty, Pairing, set Union, Power, Infinity, over the set world of it, also it proves Substitution. It can also prove class comprehension scheme. So it appears to prove all axioms of $\sf MK$-$\sf Reg.$-$\sf Choice$.

Is this theory consistent?

If so, is it equivalent to Bernay's reflection?