The principle of finite choice for a single set family (ZF)

Question

Is the below a correct proof of the fact that it is possible to choose from a single-element family in ZF (no axiom of choice!) set theory? If it is not, what is the exact point at which it breaks?
Definition. $(a,b) := \{\{a, b\}, \{b\}\}$
Axioms.
1. Axiom of pairing. $\forall A \forall B \exists C \forall D[D \in C \iff (D=A \lor D=B)]$
2. Axiom of union. $\forall A \exists B \forall C [C \in B \iff \exists D (C \in D\ \land D \in A)]$
3. Axiom of extensionality. $\forall A \forall B [\forall X (X \in A \iff X \in B) \implies A=B]$
Theorem. Let $X \ne \emptyset$, and let $F = \{X\}$ be a single-element family consisting of $X$. There exists a function $f: F \rightarrow \bigcup F$, such that $f(X)$ is an element of $X$.
Proof.
We treat $X$ as given.
From the assumption that $X \ne \emptyset$ , we have
$$\neg (\forall A [\neg (A \in X)] \ (1)$$
By the rules of FOL: $$\exists A (A \in X) \ (2)$$
By the axiom of pairing: $$\exists \{A, A\} (A \in X) \ (3)$$ By the axiom of extensionality: $$\exists \{A\} (A \in X)\ (4)\ $$ By the axiom of pairing and the existence of $X$: $$\exists \{X\}\ (5)$$ By the axiom of pairing, existence of $X$ and (2): $$\exists (A \in X) \exists \{ X, A \}\ (6)$$ By the axiom of pairing, (5) and (6) $$\exists (A \in X) \exists \{\{X\}, \{X, A\}\} \ (7)$$ By the definition of an ordered pair: $$\exists (A \in X) \exists \{(X, A) \}\ (8)$$ Now, the set ${ (X, A) }$ is exactly the desired function.

Answer 1

Nice! Four remarks.

• I think you mistyped in the definition of ordered pair: you used $(a,b)=\{\{a\},\{a,b\}\}$ at the end of your proof.
• (4) follows already from the axiom of pairing.
• You didn't actually use (3) or (4) so you can leave them out!
• To be fully precise, $\{(X,A)\}$ as in (8) is the desired function, not $(X,A)$.