| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > snex | Structured version Visualization version GIF version | ||
| Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5383. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) |
| Ref | Expression |
|---|---|
| snex | ⊢ {𝐴} ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | snexg 5435 | . 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V) | |
| 2 | snprc 4717 | . . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅) | |
| 3 | 2 | biimpi 216 | . . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅) |
| 4 | 0ex 5307 | . . 3 ⊢ ∅ ∈ V | |
| 5 | 3, 4 | eqeltrdi 2849 | . 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V) |
| 6 | 1, 5 | pm2.61i 182 | 1 ⊢ {𝐴} ∈ V |
| Copyright terms: Public domain | W3C validator |