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

Note: $``W"$ is a primitive constant symbol.

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(y))$

3.Set Comprehension: $x_1,..,x_n \in W \to \\ [ \forall x (\varphi(x) \to x \subseteq W) \leftrightarrow \forall x (\varphi(x) \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 comprehension 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 opinion, this kind of axiomatization is ideal, I think it's one of the most elegant ones. There is no substantial dispute over axioms 1 and 4. 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. Axiom 5 is a stretch of choice to all classes, which is done in versions of Morse-Kelley and NBG, so it's encountered in systems that are considered fairly standard about classes and sets. All axioms are clean and fairly natural.

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