The standard axiom of choice states that every set of non-empty sets has a choice function. And the axiom of global choice states that every class of non-empty sets has a choice function. But I’m wondering how strong a choice axiom is required to get a choice function for a set-sized collection of classes. Let me explain.
Let $X$ be a set, and let $\phi(x,y)$ be a formula such that for all $x\in X$, there exists a set $y$ such that $\phi(x,y)$. Then my question is, what is required to prove that there exists a set $Y$ and a function $f:X\rightarrow Y$ such that $\phi(x,f(x))$ for all $x\in X$?
Is the standard axiom of choice sufficient to prove this?