MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snprc Structured version   Visualization version   GIF version

Theorem snprc 4196
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.)
Assertion
Ref Expression
snprc 𝐴 ∈ V ↔ {𝐴} = ∅)

Proof of Theorem snprc
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 velsn 4140 . . . 4 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21exbii 1763 . . 3 (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3 neq0 3888 . . 3 (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4 isset 3179 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
52, 3, 43bitr4i 290 . 2 (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
65con1bii 344 1 𝐴 ∈ V ↔ {𝐴} = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194   = wceq 1474  wex 1694  wcel 1976  Vcvv 3172  c0 3873  {csn 4124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-nul 3874  df-sn 4125
This theorem is referenced by:  snnzb  4197  rabsnif  4201  prprc1  4242  prprc  4244  unisn2  4717  snexALT  4773  snex  4830  posn  5100  frsn  5102  relimasn  5394  elimasni  5398  inisegn0  5403  dmsnsnsn  5517  sucprc  5703  dffv3  6084  fconst5  6354  1stval  7038  2ndval  7039  ecexr  7611  snfi  7900  domunsn  7972  snnen2o  8011  hashrabrsn  12974  hashrabsn01  12975  hashrabsn1  12976  elprchashprn2  12997  hashsn01  13017  hash2pwpr  13065  efgrelexlema  17931  usgra1v  25685  cusgra1v  25756  1conngra  25969  eldm3  30711  opelco3  30729  fvsingle  31003  unisnif  31008  funpartlem  31025  bj-sngltag  31960  bj-restsnid  32017  wopprc  36411  uneqsn  37137  usgr1v  40477  1conngr  41356  frgr1v  41436
  Copyright terms: Public domain W3C validator