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

Note: “$W$” is a primitive constant symbol.

$\DeclareMathOperator\elm{elm}$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))$; where $x$ doesn't occur in formula $\phi(y)$.

3. **Set Comprehension:** 
$x_1,\dotsc,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 $\operatorname{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?