Kuratowski Definition of Ordered Pairs, ZFC I came accross the elegant definition given by Kuratowski of an ordered pair which is:
$$(x,y) := \{\{x\},\{x,y\}\}$$
and wondered, if the existence of this set presupposes (the axioms of) ZFC?
 A: Only the pair axiom: if $a$ and $b$ are entities (sets), then there is a set with elements exactly $a$ and $b$:

$\forall a,b\ \exists c:\ \forall x\,(x\in c \Leftrightarrow x=a\lor x=b)$

Use it for $a=b=x$ for the existence of $\{x\}$ and $a=x,\ b=y$ for $\{x,y\}$. Finally for $a=\{x\},\ b=\{x,y\}$.
As Miha commented, the axiom of extensionality is also needed for the uniqueness of this definition and for the well behaviour ($\langle x,y\rangle=\langle u,v\rangle \iff x=u\ \land\ y=v$).
A: Not all axiomatizations of ZFC include the axiom of pairing. But instead you could use the following:
Empty set + Power set + One instance of the replacement axiom (we actually prove the pairing axiom, and proceed as in Berci's answer):


*

*Start by taking two iterations of the power set on the empty set, we have a set with two elements: $\cal P(P(\varnothing))=\{\varnothing,\{\varnothing\}\}=\{\varnothing,P(\varnothing)\}$

*Now consider the following axiom from the replacement schema, defined by the formula: $$\varphi(x,y,u,v):= (x=\varnothing\rightarrow y=u)\lor (x=\mathcal P(\varnothing)\rightarrow y=v)$$
It is not hard to see that plugging in two parameters, $u$ and $v$ the formula is functional when applying it to the set $\cal P(P(\varnothing))$. Therefore by the replacement axiom for $\varphi$ we have that whenever we apply two parameters $u,v$ the collection $\{u,v\}$ is a set.

*That is to say, for every two elements $u,v$ the pair $\{u,v\}$ exists. From here Berci's answer follows. 
Note that we can directly write a formula whose "range" is the ordered pair $(u,v)$ as defined by Kuratowski, but it's about the same.
