The point of the Axiom of Choice is that oftentimes a mathematician finds him- or herself at a point where infinitely many specific objects must be gathered up all at once in order to continue a proof/construction.
In the statement as given, we have a family of nonempty sets $\{ A_i : i \in I \}$, and we want to pick a unique representative from each $A_i$, this is our function $f : I \to \bigcup_{i \in I} A_i$ ($f$ "picks" $f(i)$ to be the unique representative from $A_i$). The Axiom of Choice says that this is unproblematic, and we can always do this.
Of course, there are certain specific instances where one can do this without appealing to the Axiom of Choice:
- if you only have to make finitely many choices; or
- if these choices can be made in a uniform manner (e.g., if I have infinitely many nonempty sets of natural numbers, I can choose the least one from each set).
More often there is no way to uniformly pick these representatives, and without appealing to some extra-logical hypothesis we cannot make the choices as required.
(There are many statements known to be equivalent to the Axiom of Choice. The most common one you see in mathematics outside of logic/set theory is Zorn's Lemma.)
You are working only with finite products, and this hold in general. In the Choice Function $\Rightarrow$ AoC direction you don't know if $D$ is nonempty, that is what you are trying to pare working only with finite products, and this hold in general. In the AoC $\Rightarrow$ Choce Function direction you need a choice function on $\mathcal{A},$ not in $D.$ Moreover, I think we need to clarify some definitions.
First one definition
Definition: Let $\mathcal{A}$ be a nonempty collection os sets. A surjective function $f$ from some set $J$ to $\mathcal{A}$ is called an indexing function for $\mathcal{A}.$ $J$ is called the index set. The collection $\mathcal{A},$ together with $f,$ is called an indexed family of sets.
I'll use your definition of axiom of choice.
Axiom of choice: For any indexed family $\{ A_\alpha \}_{\alpha \in J}$ of nonempty sets, with $J \neq 0,$ the cartesian product
$$ \prod_{\alpha \in J} A_\alpha$$
is not empty. Recall that the cartesian product is the set of all functions
$$ \mathbf{x}:J \to \bigcup_{\alpha \in J}A_\alpha$$
such that $\mathbf{x}(\alpha) \in A_\alpha$ for all $\alpha \in J.$
Now,
Existence of a choice function: Given a collection $\mathcal{A}$ of nonempty sets, there exists a function
$$ c: \mathcal{A} \to \bigcup_{A \in \mathcal{A}}A$$
such that $c(A)$ is an element of $A: c(A)\in A$ for each $A \in \mathcal{A}.$
Axiom of choice $\Rightarrow$ Existence of choice function.
We are assuming that for any indexed family $\{ A_\alpha \}_{\alpha \in J}$ of nonempty sets, with $J \neq 0,$ the cartesian product $ \prod_{\alpha \in J} A_\alpha$ is not empty. Let $\mathcal{A}$ be a collection of nonempty sets. We have to prove that there exists a function $ c: \mathcal{A} \to \bigcup_{A \in \mathcal{A}}A$ such that $c(A) \in A$ for each $A \in \mathcal{A}.$ We first index $\mathcal{A}$: let $J=\mathcal{A}$ and $f:\mathcal{A} \to \mathcal{A}$ given by $f(A)=A.$ Then $\{A\}_{A \in \mathcal{A}}$ is an indexed family of sets, so we can consider its cartesian product $\prod_{A \in \mathcal{A}}A.$ By hypothesis, this product is nonempty, so there exists a function
$$ \mathbf{x}: \mathcal{A} \to \bigcup_{A \in \mathcal{A}}A$$
such that $\mathbf{x}(A) \in A$ for each $A \in \mathcal{A}.$ Then $c=\mathbf{x}$ is the function we were looking for.
Existence of choice function $\Rightarrow$ Axiom of choice
Now we are assuming that the existence of choice function, and let $\{A_\alpha \}_{\alpha \in J}$ be an indexed family of nonempty sets, with $J \neq 0.$ This means that there is a nonempty collection of sets $\mathcal{A}$ and there is an indexing (i.e. surjective) function $f:J \to \mathcal{A}$ such that $f(\alpha)=A_\alpha \in \mathcal{A}$ for each $\alpha \in J.$ By the existence of choice function, there is a function $c:\mathcal{A} \to \bigcup_{A \in \mathcal{A}}A$ such that $c(A) \in A$ for each $A \in \mathcal{A}.$ Thus
the function
$$ \mathbf{x}:= c \circ f : J \to \mathcal{A} = \bigcup_{\alpha \in J}A_\alpha$$
satisfies $\mathbf{x}(\alpha)=c(f(\alpha))=c(A_\alpha) \in A_\alpha$ for each $\alpha \in J,$ so the product $\prod_{\alpha \in J}A_\alpha$ is nonempty.
Best Answer
Your confusion here reminds me of the old saying "The axiom of choice is clearly true, the well-ordering principle is clearly false, and who can say about Zorn's lemma?"
While for any $\alpha$, you can choose an $x_\alpha \in X_\alpha$, you need the axiom of choice to show that this can be stitched together into a full choice function that is simultaneously valid for all $\alpha$. In other words, the axiom of choice takes you from the statement $\forall \alpha(\exists x_\alpha \in X\alpha)$ to the statement $\exists f(\forall\alpha(f(\alpha) \in X_\alpha))$