LET ZF be extended with class and set predicates, and extend the theory with a class abstraction schema so that for all formulas $\phi$: $$\forall \vec{z}\exists Y(Cls(Y)\wedge \forall x(x\in Y\leftrightarrow \phi(\vec{z},x)))$$ Let us call the theory $ZFC^{Cls}$. We know that many classes in $ZFC^{Cls}$ are proper classes, such as Russell's class $R=\{x|x\notin x\}$. What happens if we instead of the usual axiom of choice have axioms which for any set s, of nonempty non-overlapping sets, just postulate a *class* Y, which has precisely one member from each member of s? For example, it seems clear that the Vitali set is not definable in $ZFC^{Cls}$. Does $ZFC^{Cls}$ extend $ZF$ in any interesting way?