*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)$  

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 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?