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 4573 | . . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
2 | 1 | exbii 1839 | . . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴) |
3 | neq0 4306 | . . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴}) | |
4 | isset 3504 | . . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
5 | 2, 3, 4 | 3bitr4i 304 | . 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V) |
6 | 5 | con1bii 358 | 1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 = wceq 1528 ∃wex 1771 ∈ wcel 2105 Vcvv 3492 ∅c0 4288 {csn 4557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-dif 3936 df-nul 4289 df-sn 4558 |
This theorem is referenced by: snnzb 4646 rmosn 4647 rabsnif 4651 prprc1 4693 prprc 4695 preqsnd 4781 unisn2 5207 snexALT 5274 snex 5322 posn 5630 frsn 5632 relsnb 5668 relimasn 5945 elimasni 5949 inisegn0 5954 dmsnsnsn 6070 sucprc 6259 dffv3 6659 fconst5 6960 1stval 7680 2ndval 7681 ecexr 8283 snfi 8582 domunsn 8655 snnen2o 8695 hashrabrsn 13721 hashrabsn01 13722 hashrabsn1 13723 elprchashprn2 13745 hashsn01 13765 hash2pwpr 13822 efgrelexlema 18804 usgr1v 26965 1conngr 27900 frgr1v 27977 n0lplig 28187 unidifsnne 30223 eldm3 32894 opelco3 32915 fvsingle 33278 unisnif 33283 funpartlem 33300 bj-sngltag 34192 bj-restsnid 34272 bj-snmoore 34299 wopprc 39505 sn1dom 39770 uneqsn 40251 |
Copyright terms: Public domain | W3C validator |