![]() |
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 4226 | . . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
2 | 1 | exbii 1814 | . . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴) |
3 | neq0 3963 | . . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴}) | |
4 | isset 3238 | . . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
5 | 2, 3, 4 | 3bitr4i 292 | . 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V) |
6 | 5 | con1bii 345 | 1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 = wceq 1523 ∃wex 1744 ∈ wcel 2030 Vcvv 3231 ∅c0 3948 {csn 4210 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-dif 3610 df-nul 3949 df-sn 4211 |
This theorem is referenced by: snnzb 4286 rabsnif 4290 prprc1 4332 prprc 4334 unisn2 4827 snexALT 4882 snex 4938 posn 5221 frsn 5223 relimasn 5523 elimasni 5527 inisegn0 5532 dmsnsnsn 5649 sucprc 5838 dffv3 6225 fconst5 6512 1stval 7212 2ndval 7213 ecexr 7792 snfi 8079 domunsn 8151 snnen2o 8190 hashrabrsn 13199 hashrabsn01 13200 hashrabsn1 13201 elprchashprn2 13222 hashsn01 13242 hash2pwpr 13296 efgrelexlema 18208 usgr1v 26193 1conngr 27172 frgr1v 27251 n0lplig 27465 eldm3 31777 opelco3 31802 fvsingle 32152 unisnif 32157 funpartlem 32174 bj-sngltag 33096 bj-restsnid 33165 bj-snmoore 33193 wopprc 37914 uneqsn 38638 |
Copyright terms: Public domain | W3C validator |