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

Theorem snprc 4560
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 4488 . . . 4 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21exbii 1829 . . 3 (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3 neq0 4229 . . 3 (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4 isset 3449 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
52, 3, 43bitr4i 304 . 2 (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
65con1bii 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