![]() |
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 4649 | . . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
2 | 1 | exbii 1843 | . . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴) |
3 | neq0 4348 | . . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴}) | |
4 | isset 3476 | . . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
5 | 2, 3, 4 | 3bitr4i 302 | . 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V) |
6 | 5 | con1bii 355 | 1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 = wceq 1534 ∃wex 1774 ∈ wcel 2099 Vcvv 3462 ∅c0 4325 {csn 4633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-dif 3950 df-nul 4326 df-sn 4634 |
This theorem is referenced by: snnzb 4727 rmosn 4728 rabsnif 4732 prprc1 4774 prprc 4776 preqsnd 4865 unisn2 5317 eqsnuniex 5365 snexALT 5387 snex 5437 posn 5767 frsn 5769 relsnb 5808 relimasn 6094 elimasni 6101 inisegn0 6108 dmsnsnsn 6231 predprc 6351 sucprc 6452 dffv3 6897 fconst5 7223 ordsuci 7817 1stval 8005 2ndval 8006 ecexr 8739 snfi 9081 snfiOLD 9082 domunsn 9165 snnen2oOLD 9261 hashrabrsn 14389 hashrabsn01 14390 hashrabsn1 14391 elprchashprn2 14413 hashsn01 14433 hash2pwpr 14495 snsymgefmndeq 19392 efgrelexlema 19747 usgr1v 29192 1conngr 30127 frgr1v 30204 n0lplig 30416 unidifsnne 32462 eldm3 35583 opelco3 35598 fvsingle 35744 unisnif 35749 funpartlem 35766 bj-sngltag 36690 bj-snex 36742 bj-restsnid 36794 bj-snmooreb 36821 wopprc 42688 safesnsupfidom1o 43084 sn1dom 43193 uneqsn 43692 vsn 48197 mofsn2 48212 |
Copyright terms: Public domain | W3C validator |