Existence of a singleton set (AC for a singleton set) If $x$ is a nonempty set, is it in general possible to prove from ZF that there exists a singleton set the only element of which is in $x$ ?
This would be the result of applying the axiom of choice to the set $\{ x\}$.
Something like this is needed in the proof that if there exists an injective function $f:x\to y$, there exists a surjective function $g:y\to x$. I have been told that this proof requires the axiom of choice, however I find that a bit strange since all you need to do is set $g(z)=f^{-1}(z)$ if $f^{-1}(z)$ exists and $g(z)=v$ for a fixed $v\in x$ otherwise. Such a function $g$ is clearly surjective, but to prove its existence one needs the existence of a set of the above mentioned kind (or a function which picks one element from x). 
 A: Since $x \neq \emptyset$ there is a $y \in x$.  By Pairing there is a set $\{ y , y \} = \{ y \}$.
In general, making finitely many choices can be done in ZF in basically the same manner: 

Suppose pairwise disjoint nonempty sets $x_1 , x_2 , \ldots , x_n$ are given.  Since $x_1 \neq \emptyset$ there is a $y_1 \in x_1$.  Since $x_2 \neq \emptyset$ there is a $y_2 \in x_2$.  .... Since $x_n \neq \emptyset$ there is a $y_n \in x_n$.  Now by applications of Pairing and Union the set $\{ y_1 , y_2 , \ldots , y_n \}$ exists, and is a choice set (transversal) for $x_1 , \ldots , x_n$.

A: Use replacement to generate from $x$ the set of $\{\{v\}\mid v\in x\}$. This is set is not empty because $x$ is not empty, then its elements are the required singletons.
Choosing from a single set does not require the axiom of choice, so you may choose $\{v\}$ from it.
Lastly you don't need the axiom of choice to prove there is a surjective inverse for injections (from nonempty sets). You need the axiom of choice to prove that there is an injective inverse to a surjection, indeed this is an equivalent formulation of the axiom of choice.
