Finite axiom of choice: how do you prove it from just ZF? The axiom of choice asserts the existence of a choice function for any family of sets F. Suppose, however, that F is finite, or even that F just has one set. Then how do we prove the existence of a choice function? 
The usual answer is that we just go from set to set, picking an element from each set. Since F is finite, this process will terminate. What I'm really wondering is how we can always choose from a single set. The informal answer seems to be just that it's possible... but this isn't an axiom, so it must be justified some other way. 
So: how do you prove from the axioms of just ZF without choice, that for any nonempty x there exists a function f:{x}->x? 
 A: The Axiom of Choice does not allow to "choose" a choice function, it only says that a choice function exists. To show that a choice function for a single nonempty set exists, you do not need to "choose" an element in the set, it is enough to show that at least one element exists (i.e. the set is nonempty). Every element in the set will give a different choice function.
What did you mean by "choosing" an element from a set? ;)
A: Although the answers already given are correct, let me add some information (essentially just rephrasing the bracketed part of Thomas Scanlon's answer) that I've found useful for students who raised this question.  Consider the problem, at the end of the original question, of "choosing" from a single set $x$.  As several people have pointed out, we are given the existential statement, "There is an element in $x$."  What should be noticed in addition is that what we want to prove is also an existential statement, "There is a choice function."  We have an explicit construction, which I'll call $C$, that will convert any element of $x$ into a choice function, namely sending any $y$ to $\{(x,y)\}$ (as in Charles Staats's comment on the original question).  If we can't explicitly define any particular $y$, then we won't be able to define any particular choice function either, but the problem doesn't require us to explicitly define a choice function; we need only prove that one exists.  And that follows, thanks to $C$, from the existence of elements in $x$.
A: To say that $x \neq \varnothing$ is exactly to assert $(\exists y) y \in x$ and the truth of this existential formula will be witnessed by some set $a$ for which $a \in x$.  Thus, the set $f := \lbrace \langle x, a \rangle \rbrace$ is a function from $\lbrace x \rbrace$ to $x$.
[I think that this point, namely that the Axiom of Choice is not used to instantiate the truth of an existential formula by naming a witness is the heart of your question.  I am not claiming that there will be a constructive choice of the witness.  It is just that if an existential formula is true, there must be a witness.]
More generally, to prove that if $F$ is a finite set of nonempty sets, then $\prod F := \lbrace f :  f \text{ a function with dom}(f) = F \text{ such that } (\forall x \in F) f(x) \in x \rbrace$ is non-empty one argues by induction.
If $F = \varnothing$, then the empty function is an element of $\prod F$.   If $\text{card}(F) = n+1$, then we may express $F = F' \cup \lbrace x \rbrace$ as  disjoint union where $\text{card}(F') = n$.   As $x \neq \varnothing$, from the calculation above we find some $f:\lbrace x \rbrace \to x$.  By induction, there is some $g \in \prod F'$.  I will leave it to you to exhibit a bijection between $\prod F$ and $(\prod F') \times \prod \lbrace x \rbrace$ and thereby complete the argument.
A: There are two finite choice theorems, the internal one and the external one, both are true in ZF.
As Charles Staats pointed out, the external version is a tautology (modulo some finite combinatorics): if $a_1,\dots,a_n$ are all nonempty, then there are $z_1 \in a_1$,...,$z_n \in a_n$ and then $\lbrace (a_1,z_1),\ldots,(a_n,z_n)\rbrace$ is the desired choice function for the family $X = \lbrace a_1,\dots,a_n \rbrace$ of nonempty sets.
The internal version "every finite family of nonempty sets has a choice function" is stronger since a model of ZF may have nonstandard finite cardinals. The proof in this case is by induction on the cardinality of the family. 
The empty family has a trivial choice function — the empty function. Suppose we know the theorem to be true for families of size $n$. Let $X$ be a family of nonempty sets with size $n+1$. Let $g:n+1\to X$ be a bijection. Let $X' = g[n]$ and $a = g(n)$. Then $X'$ is a family of nonempty sets of size $n$, which therefore has a choice function $f':X' \to \bigcup X'$. Since $a$ is nonempty, we can find $z \in a$ and hence $f = f' \cup \lbrace (a,z) \rbrace$ is a choice function for the original family $X$.
