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 |
| 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 |