$\DeclareMathOperator\Cls{Cls}\newcommand{\ZFC}{\mathrm{ZFC}}$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 $\mathrm{ZF}$ in any interesting way?