| 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 4642 | . . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
| 2 | 1 | exbii 1848 | . . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴) |
| 3 | neq0 4352 | . . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴}) | |
| 4 | isset 3494 | . . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
| 5 | 2, 3, 4 | 3bitr4i 303 | . 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V) |
| 6 | 5 | con1bii 356 | 1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 = wceq 1540 ∃wex 1779 ∈ wcel 2108 Vcvv 3480 ∅c0 4333 {csn 4626 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-dif 3954 df-nul 4334 df-sn 4627 |
| This theorem is referenced by: snnzb 4718 rmosn 4719 rabsnif 4723 prprc1 4765 prprc 4767 preqsnd 4859 unisn2 5312 eqsnuniex 5361 snexALT 5383 snex 5436 posn 5771 frsn 5773 relsnb 5812 relimasn 6103 elimasni 6109 inisegn0 6116 dmsnsnsn 6240 predprc 6359 sucprc 6460 dffv3 6902 fconst5 7226 ordsuci 7828 1stval 8016 2ndval 8017 ecexr 8750 snfi 9083 snfiOLD 9084 domunsn 9167 snnen2oOLD 9264 hashrabrsn 14411 hashrabsn01 14412 hashrabsn1 14413 elprchashprn2 14435 hashsn01 14455 hash2pwpr 14515 snsymgefmndeq 19412 efgrelexlema 19767 usgr1v 29273 1conngr 30213 frgr1v 30290 n0lplig 30502 unidifsnne 32554 eldm3 35761 opelco3 35775 fvsingle 35921 unisnif 35926 funpartlem 35943 bj-sngltag 36984 bj-snex 37036 bj-restsnid 37088 bj-snmooreb 37115 wopprc 43042 safesnsupfidom1o 43430 sn1dom 43539 uneqsn 44038 vsn 48731 mofsn2 48754 |
| Copyright terms: Public domain | W3C validator |