How to prove that one can pull an existential quantification out of a universal quantification using a cartesian product of the quantified elements? Assume that $A$ is an index set and $\{ B_a \}_{a \in A}$ is a family of sets indexed by the elements of $A$. Then, I would like to prove the following identity:
$$
\forall a \in A (\exists b \in B_a (P(a, b)))
\Longleftrightarrow
\exists c \in \prod_{a \in A} B_a (\forall a \in A (P(a, c_a)))
$$
Going from left to right, the idea is that for all $a \in A$ there is a $b \in B_a$ satisfying $P(a, b)$. Let's call that one $b_a$. Then $c = (b_a | a \in A)$ (the ordered tuple consisting of each $b_a$) will be an element of $\prod_{a \in A} B_a$ such that for all $a \in A$, $c_a$ will simply be $b_a$ and so by construction of $b_a$, $P(a, c_a)$ will hold.
Going from right to left, if we assume that there exists such a $c \in \prod_{a \in A} B_a$, we can, for all $a \in A$, easily construct a $b \in B_a$ that satisfies $P(a, b)$ by simply choosing $b = c_a$.
Unfortunately, I have no idea how to formalize this proof as it feels very "intuitive" to me. Furthermore, it "feels" like this statement should have a simple proof that goes in both directions, but I can't seem to unify the two directions of the proof into one proof.
How do I formally write down the proof of this statement? Is there an elegant proof of this statement which works in both directions?
 A: Since my comments have multiplied, I’ll go ahead and answer the question.
The right-to-left implication is indeed, as OP shows, quite trivial to prove. The left-to-right implication, on the other hand, is equivalent to the axiom of choice.
The statement of the axiom of choice I will use is:

Suppose we have a set $A$ and an indexed family $\{B_a\}_{a \in A}$. Suppose for all $a \in A$, there is some element of $B_a$. Then there is some element of $\prod\limits_{a \in A} B_a$.

For suppose the left-to-right implication always holds. Then consider some indexed family $\{B_a\}_{a \in A}$ of sets, where for all $a \in A$, there is some $b \in B_a$. Let $P(a, b) :\equiv \top$; then we have $\forall a \in A \exists b \in B_a (P(a, b))$. Then there is some $c \in \prod\limits_{a \in A} B_a$. We have proved choice.
Conversely, assume the axiom of choice, and consider some indexed family $\{B_a\}_{a \in A}$ such that $\forall a \in A \exists b \in B_a (P(a, b))$. Then define $D_a = \{b \in B_a \mid P(a, b)\}$ using the axiom scheme of separation (the weaker axiom of $\Delta_0$-separation suffices when $P(a, b)$ is $\Delta_0$). Then each $D_a$ has an element, so by the axiom of choice, there is some $c \in \prod\limits_{a \in A} D_a \subseteq \prod\limits_{a \in A} B_a$. We see immediately that for all $a \in A$, we must have $P(a, c_a)$ since $c_a \in D_a$. $\square$
We know that the axiom of choice does not follow from the other axioms of set theory (unless these other axioms of set theory are themselves inconsistent - let’s hope that’s not true, since it would be a major crisis for mathematics). So we cannot prove the left-to-right implication without using the axiom of choice, since this would let us prove the axiom of choice itself from set theory’s other axioms, which cannot be done.
With some usual axioms, we can strengthen our result even further. Recall the axiom scheme of strong collection, which states:

Suppose that for all $a \in A$, there is some $b$ such that $P(a, b)$. Then there exists some set $B$, which satisfies the following two properties: (1) for all $a \in A$, there is some $b \in B$ such that $P(a, b)$, and (2) for all $b \in B$, there is some $a \in A$ such that $P(a, b)$.

We assume the axiom scheme of strong collection (which I just call “collection”), together with the axiom of choice. Then we have the following:

Suppose that for all $a \in A$, there exists some $b$ such that $P(a, b)$. Then there is some function $f$ with domain $A$ such that for all $a \in A$, we have $P(a, f(a))$.

Proof: define $Q(a, b) :\equiv \exists c (b = (a, c) \land P(a, c))$. Clearly, $\forall a \in A \exists b (Q(a, b))$. By the axiom scheme of collection, we can find some set $B$ such that $\forall a \in A \exists b \in B (Q(a, b))$ and such that $\forall b \in B \exists a \in A (Q(a, b))$.
Now define $B_a = \{c \mid \exists a \in A ((a, c) \in B)\}$ - this definition works using replacement, which follows from collection. Then $\forall a \in A \exists b \in B_a (P(a, b))$. In particular, every $B_a$ has an element. So there is some $f \in \prod\limits_{a \in A} B_a$. Furthermore, we see that $\forall a \in A \forall b \in B_a (P(a, b))$. So we have found the $f$ we are looking for. $\square$
The axiom scheme of strong collection follows from the combination of replacement, the full law of excluded middle, and foundation. The fact that foundation is apparently necessary is quite curious and intriguing.
Technical note for people who love logic: When one is dealing with intuitionist set theories (where the full law of excluded middle does not hold) and not assuming the full strength of the axiom scheme of separation, one can typically add the scheme of full collection “for free” - there is a broad class $C$ of mathematical statements where you can algorithmically transform a proof of some statement in $C$ which uses strong collection into a proof of the same statement which doesn’t use it. Adding the axiom of choice then gives you a rather unusual situation - you can prove a weak version of the law of excluded middle, that any set either has an element or is empty, but you cannot prove all instances of excluded middle.
A: I think I have discovered a proof.
Assume that $A$ is an index set and $\{ B_a \}_{a \in A}$ is a family of sets indexed by the elements of $A$.
The cartesian product in this case will be:
$$ \prod_{a \in A} B_a = \{ c \mid \forall a \in A (c_a \in B_a) \} $$
Then:
\begin{equation}
\begin{array}{*2{>{\displaystyle}c}}
                    & \forall a \in A (\exists b \in B_a (P(a, b))) \\
\Longleftrightarrow & \forall a \in A (\exists b (b \in B_a \land P(a, b))) \\
\Longleftrightarrow & \exists c (\forall a \in A (c_a \in B_a \land P(a, c_a))) \\
\Longleftrightarrow & \exists c (\forall a \in A (c_a \in B_a) \land \forall a \in A (P(a, c_a))) \\
\Longleftrightarrow & \exists c \in \prod_{a \in A} B_a (\forall a \in A (P(a, c_a))) \\
\end{array}
\end{equation}
