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 { 𝐴 } ∈ V

Proof

Step Hyp Ref Expression
1 dfsn2 { 𝐴 } = { 𝐴 , 𝐴 }
2 preq12 ( ( 𝑥 = 𝐴𝑥 = 𝐴 ) → { 𝑥 , 𝑥 } = { 𝐴 , 𝐴 } )
3 2 anidms ( 𝑥 = 𝐴 → { 𝑥 , 𝑥 } = { 𝐴 , 𝐴 } )
4 3 eleq1d ( 𝑥 = 𝐴 → ( { 𝑥 , 𝑥 } ∈ V ↔ { 𝐴 , 𝐴 } ∈ V ) )
5 zfpair2 { 𝑥 , 𝑥 } ∈ V
6 4 5 vtoclg ( 𝐴 ∈ V → { 𝐴 , 𝐴 } ∈ V )
7 1 6 eqeltrid ( 𝐴 ∈ V → { 𝐴 } ∈ V )
8 snprc ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
9 8 biimpi ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
10 0ex ∅ ∈ V
11 9 10 eqeltrdi ( ¬ 𝐴 ∈ V → { 𝐴 } ∈ V )
12 7 11 pm2.61i { 𝐴 } ∈ V