Notation: Let $\phi$ be any formula in $ \small \sf FOL$$\small(=,\in, W)$; let $\varphi$ be any formula in $\small\sf FOL$$\small (=,\in)$ having $x$ free, and whose parameters are among $x_1,..,x_n$.

Define: $elm(y)\iff \exists z (y \in z)$

Where $``elm"$ is short for "..is an element"

Axioms:

1.Extensionality: $\forall z (z \in x \leftrightarrow z \in y) \to x=y$

2.Class Comprehension: $\exists x \forall y (y \in x \leftrightarrow elm(y) \land \phi)$

3.Set Comprehension: $x_1,..,x_n \in W \to [ \forall x (\varphi \to x \subseteq W) \leftrightarrow \forall x (\varphi \to x \in W)]$

4.Foundation: $x \neq \emptyset \to \exists y \in x (y \cap x = \emptyset)$

5.Choice over all classes.

The basic two axioms of this theory are the two schemes, all the rest of axioms are indeed interpretable from them. $W$ stands for the class of all sets, that's why the predicate $elm$ is used here instead of the usual denotation of it as $set$ in Morse-Kelley class theory.

In my own personal opinion, this kind of axiomatization is ideal, I think it's of the most elegant ones. There is no dispute over axioms 1,4,and 5. Schema 2 is the most natural principle about classes. Schema 3 technically sums up all of what's in standard set theory in a neat manner. All axioms are very clean and fairly natural.

Question: What's the exact consistency strength of this theory?