A pair of identical elements is a singleton

Statement

Let $t$ be a set. By the axiom of pairing we may construct a unique (unordered) pair, which up until now we have denoted by $\{t,t\}$. We now show that $\{t,t\}$ is a singleton, thus justifying the notation:

• $\{t\}$ for a pair consisting of the same thing for both parts.

Formally we must show:

• $\exists x[x\in\{t,t\}\wedge\forall y(y\in\{t,t\}\rightarrow y\eq x)]$ (as per definition of singleton

Proof of claim

[<collapsible-expand>]

Recall the definition: for singleton

Let $X$ be a set. We call $X$ a singleton if:

• $\exists t[t\in X\wedge\forall s(s\in X\rightarrow s\eq t)]$^Caveat:See:
  • In words: $X$ is a singleton if: there exists a thing such that ( the thing is in $X$ and for any stuff ( if that stuff is in $X$ then the stuff is the thing ) )

More concisely this may be written:

• $\exists t\in X\forall s\in X[t\eq s]$

TODO: When the paring axiom has a page, do the same thing

• $\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 $A$ and $B$ are $t$ and $C$ is the (it turns out unique) set $\{t,t\}$
• To show they are equivalent we must use the axiom of extensionality
  • TODO: until it has a page, use:
    $\forall X\forall Y(\forall u(u\in X\leftrightarrow u\in Y)\rightarrow X\eq Y)$ (to compare sets $X$ and $Y$

Proof body

Grade: A*

This page requires one or more proofs to be filled in, it is on a to-do list for being expanded with them.

Please note that this does not mean the content is unreliable. Unless there are any caveats mentioned below the statement comes from a reliable source. As always, Warnings and limitations will be clearly shown and possibly highlighted if very important (see template:Caution et al).
The message provided is:

Would be good to have.

I did it on paper with paring given slightly differently:

• $\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

This proof has been marked as an page requiring an easy proof