One formulation of the axiom of choice is as follows:
Let $φ(x,y)$ be a formula, and let $X$ and $Y$ be sets such that for every $x\in X$, there exists at least one $y\in Y$ for which $φ(x,y)$ is true. Then there is a function $f:X\rightarrow Y$ such that $φ(x,f(x))$ is true for all $x\in X$.
I know that the choice of $f(x)$ in any formulation of the axiom of choice is restricted to a set (namely, Y, in this example). However, regarding this specific formulation of AOC, I have the following confusion:
What if we don't have a set $Y$ to contain all those y for which $φ(x,y)$ is true?
More precisely, is the following still a true statement?
Let $φ(x,y)$ be a formula, and let $X$ be a set such that for every $x\in X$, there exists at least one set y (in ZFC, everything we consider is a set) for which $φ(x,y)$ is true. Then there exists a function $f$ with $dom(f)=X$ such that $φ(x,f(x))$ is true for all $x\in X$.
Sorry for the language barrier. I hope I have expressed my thought clearly.
More information:In Enderton's book, there is one formulation of AOC (let's call it AOC(Ⅰ)):For every relation $R$, there is some function $f\subseteq R$ such that $dom(f)=dom(R)$.(Note:this definition of a function does not include the notion of codomian.In other words, a function is just a set of ordered pairs which satisfies the "vertical line test".)
Notice that in order to find such a function $f$, for each $x\in dom(R)$, we need to choose a corresponding $f(x)$ in the set $ran(R)$.This is why I indicated in the preceding paragraph that the choice of $f(x)$ is restricated to some set.
However, if that proposition in bold type is true, then I think we can extend AOC(Ⅰ) informally as follows:For every "relation-class" $R$ with $dom(R)$ being a set, there is some function $f\subseteq R$ such that $dom(f)=dom(R)$.
Here a "relation-class" (which can only be treated intuitively and informaly in ZF) is a "class" of ordered pairs that may or may not be a set. This is not a proposition in ZF, but some intuitive understanding of mine.
To prove this informal proposition, take $φ(x,y)$ to be $(x,y)\in R$.
The thing here is that Replacement axioms guarantee that such $Y$ exist. At least if you are working in $\sf ZF$. This is much closer, as a whole, to the Collection schema, than to the Replacement schema, as we are not requiring uniqueness. But this is not a problem. The two are equivalent over $\sf ZF-Rep$.
For every $x$, there is a set of minimal rank $\alpha$ such that there is some $y$ for which $\varphi(x,y)$ holds. Let $Y_x$ be the set $\{y\in V_{\alpha+1}\mid\varphi(x,y)\}$, then by Separation, this is a set. Apply Replacement to the function $x\mapsto Y_x$, which is now uniquely determined, then $\{Y_x\mid x\in X\}$ is a set. Finally, let $Y=\bigcup\{Y_x\mid x\in X\}$.
Alternatively, we can just map $x$ to that minimal $\alpha_x$, then take $\alpha=\sup\{\alpha_x\mid x\in X\}$ and take $Y$ to be $V_{\alpha+1}$. In either case, Replacement save the day.
If you are working in weaker theories where Collection and Replacement do not hold, then it is true that these two formulations need not be equivalent.