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	|- { A } e. _V

Proof

Step	Hyp	Ref	Expression
1		dfsn2	|- { A } = { A , A }
2		preq12	|- ( ( x = A /\ x = A ) -> { x , x } = { A , A } )
3	2	anidms	|- ( x = A -> { x , x } = { A , A } )
4	3	eleq1d	|- ( x = A -> ( { x , x } e. _V <-> { A , A } e. _V ) )
5		zfpair2	|- { x , x } e. _V
6	4 5	vtoclg	|- ( A e. _V -> { A , A } e. _V )
7	1 6	eqeltrid	|- ( A e. _V -> { A } e. _V )
8		snprc	|- ( -. A e. _V <-> { A } = (/) )
9	8	biimpi	|- ( -. A e. _V -> { A } = (/) )
10		0ex	|- (/) e. _V
11	9 10	eqeltrdi	|- ( -. A e. _V -> { A } e. _V )
12	7 11	pm2.61i	|- { A } e. _V