![]() |
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 4607 | . . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
2 | 1 | exbii 1851 | . . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴) |
3 | neq0 4310 | . . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴}) | |
4 | isset 3461 | . . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
5 | 2, 3, 4 | 3bitr4i 303 | . 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V) |
6 | 5 | con1bii 357 | 1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 = wceq 1542 ∃wex 1782 ∈ wcel 2107 Vcvv 3448 ∅c0 4287 {csn 4591 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-dif 3918 df-nul 4288 df-sn 4592 |
This theorem is referenced by: snnzb 4684 rmosn 4685 rabsnif 4689 prprc1 4731 prprc 4733 preqsnd 4821 unisn2 5274 eqsnuniex 5321 snexALT 5343 snex 5393 posn 5722 frsn 5724 relsnb 5763 relimasn 6041 elimasni 6048 inisegn0 6055 dmsnsnsn 6177 predprc 6297 sucprc 6398 dffv3 6843 fconst5 7160 ordsuci 7748 1stval 7928 2ndval 7929 ecexr 8660 snfi 8995 domunsn 9078 snnen2oOLD 9178 hashrabrsn 14279 hashrabsn01 14280 hashrabsn1 14281 elprchashprn2 14303 hashsn01 14323 hash2pwpr 14382 snsymgefmndeq 19183 efgrelexlema 19538 usgr1v 28246 1conngr 29180 frgr1v 29257 n0lplig 29467 unidifsnne 31505 eldm3 34373 opelco3 34388 fvsingle 34534 unisnif 34539 funpartlem 34556 bj-sngltag 35483 bj-snex 35535 bj-restsnid 35587 bj-snmooreb 35614 wopprc 41383 safesnsupfidom1o 41763 sn1dom 41872 uneqsn 42371 vsn 46970 mofsn2 46985 |
Copyright terms: Public domain | W3C validator |