![]() |
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 4488 | . . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
2 | 1 | exbii 1829 | . . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴) |
3 | neq0 4229 | . . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴}) | |
4 | isset 3449 | . . 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 1522 ∃wex 1761 ∈ wcel 2081 Vcvv 3437 ∅c0 4211 {csn 4472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-v 3439 df-dif 3862 df-nul 4212 df-sn 4473 |
This theorem is referenced by: snnzb 4561 rmosn 4562 rabsnif 4566 prprc1 4608 prprc 4610 preqsnd 4696 unisn2 5107 snexALT 5174 snex 5223 posn 5523 frsn 5525 relsnb 5561 relimasn 5828 elimasni 5832 inisegn0 5837 dmsnsnsn 5952 sucprc 6141 dffv3 6534 fconst5 6835 1stval 7547 2ndval 7548 ecexr 8144 snfi 8442 domunsn 8514 snnen2o 8553 hashrabrsn 13581 hashrabsn01 13582 hashrabsn1 13583 elprchashprn2 13605 hashsn01 13625 hash2pwpr 13680 efgrelexlema 18602 usgr1v 26721 1conngr 27660 frgr1v 27742 n0lplig 27951 unidifsnne 29985 eldm3 32606 opelco3 32627 fvsingle 32991 unisnif 32996 funpartlem 33013 bj-sngltag 33919 bj-restsnid 33996 bj-snmoore 34024 wopprc 39131 sn1dom 39396 uneqsn 39877 |
Copyright terms: Public domain | W3C validator |