Theorem snex

Description: A singleton is a set. Theorem 7.12 of Quine p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT . (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 19-May-2013) (Proof modification is discouraged.)

	Ref	Expression
Assertion	snex	$$⊢\left\{A\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		dfsn2	$$⊢\left\{A\right\}=\left\{A,A\right\}$$
2		preq12	$$⊢\left(x=A\wedge x=A\right)\to \left\{x,x\right\}=\left\{A,A\right\}$$
3	2	anidms	$$⊢x=A\to \left\{x,x\right\}=\left\{A,A\right\}$$
4	3	eleq1d	$$⊢x=A\to \left(\left\{x,x\right\}\in \mathrm{V}\leftrightarrow \left\{A,A\right\}\in \mathrm{V}\right)$$
5		zfpair2	$$⊢\left\{x,x\right\}\in \mathrm{V}$$
6	4 5	vtoclg	$$⊢A\in \mathrm{V}\to \left\{A,A\right\}\in \mathrm{V}$$
7	1 6	eqeltrid	$$⊢A\in \mathrm{V}\to \left\{A\right\}\in \mathrm{V}$$
8		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
9	8	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
10		0ex	$$⊢\varnothing \in \mathrm{V}$$
11	9 10	eqeltrdi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}\in \mathrm{V}$$
12	7 11	pm2.61i	$$⊢\left\{A\right\}\in \mathrm{V}$$