Does a “backwards” choice function imply the Axiom of Choice?

One of my favorite formulations of the Axiom of Choice is that for any nonempty family $A$ of nonempty sets, there is a choice function $F\colon A\to\cup A$ such that $F(X)\in X$ for each $X\in A$.

Using this, I was able to prove that there is also a function $f\colon\cup A\to A$ such that $x\in f(x)\in A$ for all $x\in\cup A$. I did this by considering any $x\in\cup A$, and letting $B_x=\{X\in A\mid x\in X\}$, and then letting $C=\{t\in\mathscr{P}(A)\mid \exists_{x\in\cup A}t=B_x\}$, i.e. $C$ is the set of all $B_x$. Now each $B_x$ is nonempty, so there is a choice function $F$ such that $F(B_x)\in B_x$ for each $B_x$. Defining $f(x)=F(B_x)$, I have $x\in f(x)\in A$ for every $x\in\cup A$. I suppose this is what I mean by a "backwards" choice function, even though it's not really one.

Is this equivalent to AC? That is, if for any set $A$, there exists a function $f\colon\cup A\to A$ such that $x\in f(x)\in A$ for all $x\in\cup A$, then AC holds? I couldn't immediately see a way to imply the Axiom of Choice, in any equivalent formulation assuming that the above is true for any set $A$. Is it just a one way implication? Thanks.

-
On the surface it seems similar to how the fact that every surjective map can be inversed to a subset of the domain, I do not recall if this is equivalent or strictly weaker than choice. (I will try to write some proof anyway.) –  Asaf Karagila May 8 '11 at 11:14
There is a chance this is a duplicate (I didn't read the question very carefully -I've got to go- so sorry if it's not): math.stackexchange.com/q/29772/1772 –  Apostolos May 8 '11 at 11:15
@Apostolos: This seems to be the inverse question. Whether this function requires choice. In here the question is if the existence of this function implies choice. –  Asaf Karagila May 8 '11 at 11:19
@Asaf: You are right, but it just happens that to answer the question Carl and I essentially provided an answer to yunone's question (and that's probably the reason I thought they were the same). –  Apostolos May 8 '11 at 12:17
@IainM: I would read "this function requires choice" as $AC \implies \exists f$ while "the existence of this function implies choice" as $\forall A \exists f \implies AC$, so they would be converses. –  Ross Millikan May 8 '11 at 12:39

An answer to a related question I gave some time ago happens to answer your question. I'm posting it here as well:

This is equivalent to the axiom of choice. Take a set $X$ of non-empty sets. Let the set $X'= X\cup\{\{x\} : x\in\bigcup X\}$ and for every $x\in\bigcup X$ take $C_x=\{y\in X' : x\in y\}$. Observe that if $x\neq y$ then $C_x\neq C_y$ since $\{x\}\in C_x$ while $\{x\}\notin C_y$. The set $A=\{C_x : x\in\bigcup X\}$ is a set through the axiom of replacement and you have that $\bigcup A=X'$. If there is a function $f:X'\to A$ satisfying the statement you wrote you have a choice function $g$ for $X$, namely $g(y)=x\iff f(y)=C_x$.

-
Thanks for your answer Apostolos. Is it necessary that $x\neq y\implies C_x\neq C_y$? –  yunone May 8 '11 at 21:20
@yunone: Yes it is, because of how $g$ is defined. Assume that we have $x\neq y$ while $C_x=C_y=C$ and there is a $z$ such that $f(z)=C$. Then we would require to somehow choose either $x$ or $y$ for $g(z)$, and it is not clear how that would be possible without using some choice. Actually when I first answered the question I link to I missed this fact as well. You can read the comments at my answer there as well as Carl's answer for a different approach that again needs some sort of coding of extra information. –  Apostolos May 8 '11 at 21:39
I see, thanks again. –  yunone May 8 '11 at 21:51

No, this construction works perfectly in ZF.

HINT: Write your $f$ as the composition: $\bigcup A \rightarrow \coprod A \rightarrow A$, where $\coprod A$ is the disjoint sum of elements of $A$.

Sorry, I answered a wrong question. I think the answer to your question is: yes, they are equivalent.

Consider any surjection $f \colon A \rightarrow B$, and, without loss of generality, assume that both $A$ and $B$ are disjoint. Then form a family $F = \{ \{a, f(a)\} \colon a \in A \}$. Since $f$ is surjective, $\bigcup F = A \cup B$. So, thanks to your axiom, there is a function $h \colon A \cup B \rightarrow F$ such that $b \in h(b)$. There is also an obvious projection $p = \{\langle t, a \rangle \colon a \in t\} \colon F \rightarrow A$ --- that is $p(\{a, b\}) = a$. Composing these two functions with the obvious injection $\iota_B \colon B \rightarrow A \cup B$ gives a section of $f$, that is $p \circ h \circ \iota_B \colon B \rightarrow A$, what is just another formulation of AC (i.e. every surjection has a section).

-
How can you go from $\bigcup A$ to $\coprod A$? –  Asaf Karagila May 8 '11 at 11:32
Sorry, I answered a wrong question. I have edited my answer, and now it should address your question correctly :-) –  Michal R. Przybylek May 8 '11 at 12:46

Yes. Define $A' = \{(a,b) : b \in a \in A\}$. Then for any $a \in A$ we have $\{a\} \in \bigcup A'$ (taking the definition of the ordered pair to be $(a,b) = \{\{a\},\{a,b\}\}$). So if $g$ is a backwards-choice function on $A'$, $g(\{a\})$ is an ordered pair $(a,f(a))$, where $f(a) \in a$. So the $f$ defined in this way is a choice function on $A$ (with the usual definition).

-