Quantification and the existence of a function

I am trying hard to understand what exactly the axiom of choice (AC) is. I think much of the confusion comes from taking AC obvious not knowing what exactly ZF implies.

AC for nonempty indexed families $(B_x )_{x \in A}$ is represented by $$ \forall x \in A:B_x \neq \varnothing \Rightarrow \exists f \in A \to \cup_{x \in A}B_x:\forall x \in A: f(x) \in B_x $$ where $X \to Y$ denote the set of all functions from $X$ to $Y$.

For example, for sets $X$ and $Y$, and a predicate $P$, the statement $$ \forall x \in X: \exists y \in Y: P(x,y) \Rightarrow \exists f \in X \to Y: \forall x \in X: P(x,f(x)) $$ is a direct consequence of AC as we can define $B_x = \{y \in Y|P(x,y)\}$. My question is, does the statement really need AC in ZF?

Yes, AC is necessary for your statement because you can also prove AC from your statement in ZF:

To see this, assume your statement $$ \forall x \in X: \exists y \in Y: P(x,y) \Rightarrow \exists f \in X \to Y: \forall x \in X: P(x,f(x)) \quad \cdots (\star) $$

Next, assume the hypotheses of AC. That is, let $(B_x)_{x \in A}$ be an indexed family and suppose for all $x \in A$, we have $B_x \neq \varnothing$. So let $x \in A$. Since $B_x \neq \varnothing$ and $B_x \subseteq \bigcup_{x \in A} B_x$, the condition $\exists y \in \bigcup_{x \in A} B_x : y \in B_x$ is satisfied. Hence, by setting

• $X := A$
• $Y := \bigcup_{x \in A} B_x$
• $P(x, y) := y \in B_x$

In your statement $(\star)$, we get the conclusion that there exists some $f \in X \to Y$ i.e. $f \in A \to \bigcup_{x \in A} B_x$ such that for all $x \in X$ i.e. $x \in A$, we have $P(x, f(x))$ i.e. $f(x) \in B_x$.

This is exactly the conclusion you need for AC.