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

$\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 Set(x)\wedge\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?

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?

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