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

Theorem snprc 3708
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, 5-Aug-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 3668 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21exbii 1572 . . 3  |-  ( E. x  x  e.  { A }  <->  E. x  x  =  A )
3 neq0 3478 . . 3  |-  ( -. 
{ A }  =  (/)  <->  E. x  x  e.  { A } )
4 isset 2805 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
52, 3, 43bitr4i 268 . 2  |-  ( -. 
{ A }  =  (/)  <->  A  e.  _V )
65con1bii 321 1  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176   E.wex 1531    = wceq 1632    e. wcel 1696   _Vcvv 2801   (/)c0 3468   {csn 3653
This theorem is referenced by:  prprc1  3749  prprc  3751  snexALT  4212  snex  4232  sucprc  4483  unisn2  4538  posn  4774  frsn  4776  relimasn  5052  elimasni  5056  dmsnsnsn  5167  dffv3  5537  fconst5  5747  1stval  6140  2ndval  6141  ecexr  6681  snfi  6957  domunsn  7027  hashsnlei  11392  efgrelexlema  15074  eldm3  24190  unisnif  24535  funpartlem  24552  wopprc  27226  inisegn0  27243  elprchashprn2  28216  usgra1v  28260  cusgra1v  28296
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-nul 3469  df-sn 3659
  Copyright terms: Public domain W3C validator