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

Theorem snprc 4095
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 4046 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21exbii 1668 . . 3  |-  ( E. x  x  e.  { A }  <->  E. x  x  =  A )
3 neq0 3804 . . 3  |-  ( -. 
{ A }  =  (/)  <->  E. x  x  e.  { A } )
4 isset 3113 . . 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 1395   E.wex 1613    e. wcel 1819   _Vcvv 3109   (/)c0 3793   {csn 4032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3474  df-nul 3794  df-sn 4033
This theorem is referenced by:  snnzb  4096  rabsnif  4101  prprc1  4142  prprc  4144  unisn2  4592  snexALT  4642  snex  4697  sucprc  4962  posn  5077  frsn  5079  relimasn  5370  elimasni  5374  dmsnsnsn  5492  dffv3  5868  fconst5  6130  1stval  6801  2ndval  6802  ecexr  7334  snfi  7615  domunsn  7686  snnen2o  7725  hashrabrsn  12443  hashrabsn01  12444  hashrabsn1  12445  elprchashprn2  12465  hashsnlei  12482  hash2pwpr  12523  efgrelexlema  16894  usgra1v  24517  cusgra1v  24588  1conngra  24802  eldm3  29388  opelco3  29404  fvsingle  29754  unisnif  29759  funpartlem  29776  wopprc  31155  inisegn0  31172  bj-sngltag  34663
  Copyright terms: Public domain W3C validator