View source for A pair of identical elements is a singleton

__TOC__
==Statement==
Let {{M|t}} be a [[set]]. By ''[[the axiom of pairing]]'' we may construct a unique (unordered) pair, which up until now we have denoted by {{M|\{t,t\} }}. We now show that {{M|\{t,t\} }} is a {{link|singleton|set theory}}, thus justifying the notation:
* {{M|\{t\} }} for a pair consisting of the same thing for both parts.
Formally we must show:
* {{M|\exists x[x\in\{t,t\}\wedge\forall y(y\in\{t,t\}\rightarrow y\eq x)]}} (as per definition of {{link|singleton|set theory}}
==Proof of claim==
{{Begin Notebox}}
'''Recall the definition: ''' for {{link|singleton|set theory}}
{{Begin Notebox Content}}
{{:Singleton (set theory)/Definition}}
{{End Notebox Content}}{{End Notebox}}
{{XXX|When the paring axiom has a page, do the same thing}}
* {{M|\forall A\forall B\exists C\forall x(x\in C\leftrightarrow x\eq A\vee x\eq B)}} this is the pairing axiom, in this case {{M|A}} and {{M|B}} are {{M|t}} and {{M|C}} is the (it turns out unique) set {{M|\{t,t\} }}
* To show they are equivalent we must use [[the axiom of extensionality]]
** {{XXX|until it has a page, use: }} {{M|\forall X\forall Y(\forall u(u\in X\leftrightarrow u\in Y)\rightarrow X\eq Y)}} (to compare sets {{M|X}} and {{M|Y}}
===Proof body===
{{Requires proof|grade=A*|msg=Would be good to have.

I did it on paper with paring given slightly differently:
* {{M|\forall A\forall B\exists C\big[A\in C\wedge B\in C\wedge\forall x[x\in C\implies (c\eq A\vee c\eq B)]\big]}}
and that worked at least, I suspect this is equivalent to paring but I really want to move forward so haven't shown this|easy=true}}
==Notes==
<references group="Note"/>
==References==
<references/>
{{Theorem Of|Set Theory|Elementary Set Theory}}