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

Theorem snprc 4645
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 4573 . . . 4 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21exbii 1839 . . 3 (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3 neq0 4306 . . 3 (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4 isset 3504 . . 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 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