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

Theorem snprc 4097
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 4047 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21exbii 1644 . . 3  |-  ( E. x  x  e.  { A }  <->  E. x  x  =  A )
3 neq0 3800 . . 3  |-  ( -. 
{ A }  =  (/)  <->  E. x  x  e.  { A } )
4 isset 3122 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
52, 3, 43bitr4i 277 . 2  |-  ( -. 
{ A }  =  (/)  <->  A  e.  _V )
65con1bii 331 1  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    = wceq 1379   E.wex 1596    e. wcel 1767   _Vcvv 3118   (/)c0 3790   {csn 4033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3120  df-dif 3484  df-nul 3791  df-sn 4034
This theorem is referenced by:  snnzb  4098  rabsnif  4102  prprc1  4143  prprc  4145  unisn2  4589  snexALT  4639  snex  4694  sucprc  4959  posn  5074  frsn  5076  relimasn  5366  elimasni  5370  dmsnsnsn  5492  dffv3  5868  fconst5  6129  1stval  6797  2ndval  6798  ecexr  7328  snfi  7608  domunsn  7679  snnen2o  7718  hashrabrsn  12420  hashrabsn01  12421  hashrabsn1  12422  elprchashprn2  12441  hashsnlei  12458  hash2pwpr  12499  efgrelexlema  16638  usgra1v  24222  cusgra1v  24293  1conngra  24507  eldm3  29125  opelco3  29142  fvsingle  29504  unisnif  29509  funpartlem  29526  wopprc  30906  inisegn0  30923  bj-sngltag  34028
  Copyright terms: Public domain W3C validator