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?