Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > snprc | Structured version Visualization version GIF version |
Description: The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of [Quine] p. 48. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
snprc | ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | velsn 4141 | . . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
2 | 1 | exbii 1764 | . . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴) |
3 | neq0 3889 | . . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴}) | |
4 | isset 3180 | . . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
5 | 2, 3, 4 | 3bitr4i 291 | . 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V) |
6 | 5 | con1bii 345 | 1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 195 = wceq 1475 ∃wex 1695 ∈ wcel 1977 Vcvv 3173 ∅c0 3874 {csn 4125 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-dif 3543 df-nul 3875 df-sn 4126 |
This theorem is referenced by: snnzb 4198 rabsnif 4202 prprc1 4243 prprc 4245 unisn2 4722 snexALT 4778 snex 4835 posn 5110 frsn 5112 relimasn 5407 elimasni 5411 inisegn0 5416 dmsnsnsn 5531 sucprc 5717 dffv3 6099 fconst5 6376 1stval 7061 2ndval 7062 ecexr 7634 snfi 7923 domunsn 7995 snnen2o 8034 hashrabrsn 13022 hashrabsn01 13023 hashrabsn1 13024 elprchashprn2 13045 hashsn01 13065 hash2pwpr 13115 efgrelexlema 17985 usgra1v 25919 cusgra1v 25990 1conngra 26203 eldm3 30905 opelco3 30923 fvsingle 31197 unisnif 31202 funpartlem 31219 bj-sngltag 32164 bj-restsnid 32221 wopprc 36615 uneqsn 37341 usgr1v 40482 1conngr 41361 frgr1v 41441 |
Copyright terms: Public domain | W3C validator |