The unordered pair $\{x,y\}$ and the singleton $\{x\}=\{x,x\}$

Let $x$ and $y$ be sets. The Axiom of Pairing: $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\exists }z\mathrm{\forall }t(t\in z\leftrightarrow (t=x\vee t=y))$ gives a set whose elements are exactly $x$ and $y$, and The Axiom of Extensionality: $\mathrm{\forall }x\mathrm{\forall }y(\mathrm{\forall }z(z\in x\leftrightarrow z\in y)\to x=y)$ shows there is only one such set; it is written $\{x,y\}$. Thus $\{x,y\}$ is the set whose elements are exactly $x$ and $y$, and $\{x\}:=\{x,x\}$, the singleton of $x$, is the set whose only element is $x$:

$t\in \{x,y\}\leftrightarrow (t=x\vee t=y),t\in \{x\}\leftrightarrow t=x\mathrm{.}$

• The pair is unordered. $t=x\vee t=y$ and $t=y\vee t=x$ are the same condition, so $\{x,y\}=\{y,x\}$, and the notation records no order. $\{a,b\}=\{c,d\}$ if and only if ($a=c$ and $b=d$) or ($a=d$ and $b=c$); in particular $\{a\}=\{c,d\}$ if and only if $a=c=d$ says exactly how much information a pair does carry, and The Kuratowski ordered pair $(a,b):=\{\{a\},\{a,b\}\}$ is the construction that recovers an order from unordered pairs alone.

• A singleton is not its element. $\{x\}$ has exactly one element, namely $x$, and $x$ and $\{x\}$ are different sets whenever they have different elements; $\{\mathrm{\varnothing }\}$ has one element while $\mathrm{\varnothing }$ has none, so the two are already distinct at the bottom of the hierarchy.