I've been trying to prove the following two formulations of the Axiom of Choice are equivalent:
Formulation 1: Given a non-empty set $A$ of non-empty sets, there is a function $f$ that maps each $x \in A$ to an element of $x$, i.e. for each $x \in A$, $f(x) \in x$.
Formulation 2: Let $A$ be a non-empty set which contains only pairwise disjoint non-empty sets. There is a set $C$ that consists of elements of elements of $A$ and contains exactly one element of each element of $A$, i.e. for each $x \in A$, $C \cap x$ is a singleton.
I had no trouble seeing formulation 1 implies formulation 2, but the other way around has confused me for some time. I came up with a solution and I'd like to know if it makes sense. Since it can be a bit extensive I'll only give an outline of the insights I've used. From now on assume formulation 2 and let $A$ be a non-empty set of non-empty sets as in formulation 1.
Step 1: Note that for every $x \in A$ there is a set $C$ such that $C \cap x$ is a singleton. This follows from the fact that one may make a partition of $\bigcup A$ with $\{x, \bigcup A - x\}$ (exception: $x = \bigcup A$, but then just consider the set $\{x\}$ instead of $\{x, \bigcup A - x\}$ in that case). Since this is a set of pairwise disjoint non-empty sets there is $C$ such that $C \cap x$ and $C \cap (\bigcup A - x)$ are singletons.
Step 2: Out of the set $A \times \bigcup A$, take the elements $(x, y)$ such that there is $C$ where $y$ is the only element of $C \cap x$. Note $y \in x$ in every such case, and that the resulting set has all elements of $A$ in its domain, since for every $x \in A$ there is at least one such $y$ by step 1. From now on we call this resulting set $B$.
Step 3: Create a partition of $B$ by comparing the elements of the first coordinate. This can be done by defining a equivalence relation in $B \times B$ where two elements are similar if their first coordinate is equal, then take the partition corresponding to that equivalence relation.
Step 4: Use formulation 2 of the AC on the partition defined above. The resulting set $C$ is a choice function as in formulation 1, since for each $x \in A$ there is one and only one $y \in x$ such that $(x,y) \in C$.
Step 1 was my main insight, but I've noticed that there may be more than one set $C$ as in formulation 2, and there was no way to choose one of them. The other steps are a way to circumvent that.
Of course there are details missing from the above, but I'd like to know if I'm on the right track. Moreover I have to admit that the solution I came up with seems sort of roundabout, even if it's valid I'd like to know if there is anything superfluous in the steps I've specified, or if there is a quicker solution that is similar in spirit.
Thanks in advance!
Your first two steps make little sense. Moreover, they run a very dangerous game with the existential quantifier.
To be specific, given any family of non-empty sets $A$, for every $x\in A$, there exists some $y$ such that $y\in x$. Now we can take the set $X$ such that $y\in X$ if and only if for some $x\in A$, $y\in x$. But then $X=\bigcup A$.
In other words, once you quantify "for every $x$ there exists $C$ such that $C\cap x$ is a singleton" there is no longer any obligation for $C$ to remain the same as your $x$ varies.
You can find several questions on this site with the actual solution, and you were, to an extent, somewhat close to the actual solution. But given the family $A$, let $B=\{\{x\}\times x\mid x\in A\}$, what can you say about the members of $B$ and how does "Formulation 2" apply here?