Metamath Proof Explorer


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