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 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 V A A V
5 zfpair2 x x V
6 4 5 vtoclg A V A A V
7 1 6 eqeltrid A V A V
8 snprc ¬ A V A =
9 8 biimpi ¬ A V A =
10 0ex V
11 9 10 syl6eqel ¬ A V A V
12 7 11 pm2.61i A V