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

Theorem snprc 4063
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  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )

Proof of Theorem snprc
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elsn 4012 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21exbii 1712 . . 3  |-  ( E. x  x  e.  { A }  <->  E. x  x  =  A )
3 neq0 3772 . . 3  |-  ( -. 
{ A }  =  (/)  <->  E. x  x  e.  { A } )
4 isset 3084 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
52, 3, 43bitr4i 280 . 2  |-  ( -. 
{ A }  =  (/)  <->  A  e.  _V )
65con1bii 332 1  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187    = wceq 1437   E.wex 1657    e. wcel 1872   _Vcvv 3080   (/)c0 3761   {csn 3998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-v 3082  df-dif 3439  df-nul 3762  df-sn 3999
This theorem is referenced by:  snnzb  4064  rabsnif  4069  prprc1  4110  prprc  4112  unisn2  4560  snexALT  4610  snex  4662  posn  4922  frsn  4924  relimasn  5210  elimasni  5214  inisegn0  5219  dmsnsnsn  5333  sucprc  5517  dffv3  5877  fconst5  6137  1stval  6809  2ndval  6810  ecexr  7379  snfi  7660  domunsn  7731  snnen2o  7770  hashrabrsn  12557  hashrabsn01  12558  hashrabsn1  12559  elprchashprn2  12579  hashsnlei  12596  hash2pwpr  12639  efgrelexlema  17398  usgra1v  25115  cusgra1v  25187  1conngra  25401  eldm3  30409  opelco3  30427  fvsingle  30692  unisnif  30697  funpartlem  30714  bj-sngltag  31545  wopprc  35855  usgr1v  39107
  Copyright terms: Public domain W3C validator