Why is Axiom of Pairing needed? I'm learning ZFC set theory and I'm very confused about the Axiom of Pairing.

Axiom of Pairing: For any $a$ and $b$ there exists a set $\{a, b\}$ that contains exactly $a$ and $b$.

It seems that this axiom can be derived from other axioms in a lot of ways. For example, consider the powerset of the powerset of $\varnothing$, which is $\{\varnothing,\{\varnothing\}\}$, and then we apply the Axiom Schema of Replacement we can get $\{a,b\}$.
I looked for Wiki. It says the "non-independence" as well.
I'm confused why the Axiom of Pairing is important and independent. Also, why do we use "pair sets" instead of "singleton sets"? It seems equivalant that we use "singleton sets" axiom and the Axiom of Union to deduce the Axiom of Pairing?
 A: Note that Replacement cannot be philosophically justified non-circularly, so philosophically you would want to distinguish between theorems that rely on Replacement and theorems that do not. Pairing is in contrast rather innocuous, and is crucial in obtaining ordered pairs (meaning definable pairing and projection) in Zermelo set theory.
Also, even if one axiom implies another, it does not imply that the weaker one is unimportant. For example, the unrestricted comprehension axiom (schema) of naive set theory entails Pairing and Union and Powerset and Replacement, but also entails contradiction. What is important is what can be justified and not usually what can imply more things.
In the case of Pairing, it captures a relatively simple notion that given any two objects $a,b$ we can form a single collection whose members must each be either equal to $a$ or $b$. 'Clearly' we can form such a conceptual collection.
It is true that if ZFC is meaningful then Replacement can be considered more fundamental than Separation and Pairing, because it not only entails them but also itself corresponds to reification of definable functions on a set, meaning that for any formula $P$ such that $\forall x \in S\ \exists! y ( P(x,y) )$ ($P$ is a definable function) there is an object $f$ representing $P$, namely $\forall x \in S\ \exists! y ( (x,y) \in f )$. Note that unrestricted reification of definable functions on a set entails a contradiction, just as unrestricted reification of definable 1-place predicates (which is precisely unrestricted comprehension) entails a contradiction.
But to give an example showing that it is not philosophically sufficient to have mere consistency, consider that PA+¬Con(PA) proves everything that PA does, and is consistent, but most logicians reject it as meaningless to the real world, unlike PA+Con(PA), which most logicians accept as true (or a good approximation) of real-world 'natural numbers'.
A: In ZFC theory the Axiom of Pairing appears rather early, so its justification need not be too complicated. In the OP's example, where he asserted the existence of $\{\emptyset,\{\emptyset\}\}$, he already invoked the Axiom of Pairing. Now, you (and the OP himself) might argue that what was invoked was the Axiom of Powerset. However, the Axiom of Powerset is meant to be invoked to construct sets of infinite depth (having infinite nested brackets). The ZFC theory describes a universe where sets are constructed inductively. Like in all metamathematical inductive formulations, you need a basis, and you need an induction hypothesis. The basis and the induction hypothesis are two different things, and one does not replace the other. In the present case, the Axiom of Pairing plays the role of the basis, while the Axiom of the Powerset plays the role of the induction hypothesis. Thus, the very example used already demonstrated the necessity of the Axiom of Pairing, for without it $\{\emptyset,\{\emptyset\}\}$ can not be claimed to be a set.
As to the Axiom Schema of Replacement, it is meant to rein in what is meant by infinity. To see this, note that while a Russell class is infinite in size and is not a set, a powerset is infinite in size and is a set. The Axiom Schema of Replacement can then be invoked to construct sets of desired sizes, as shown by the OP. It is an important and integral part of ZFC theory. With it, you can quickly assert the existence of a set without having to build it from the ground up. This frees you from the worries of having sets that are infinite yet not "too large". Thus, both the Axiom of Pairing and the Axiom Schema of Replacement have their places. One does not make the other redundant.
