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

Theorem snprc 4048
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 3994 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21exbii 1729 . . 3  |-  ( E. x  x  e.  { A }  <->  E. x  x  =  A )
3 neq0 3754 . . 3  |-  ( -. 
{ A }  =  (/)  <->  E. x  x  e.  { A } )
4 isset 3061 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
52, 3, 43bitr4i 285 . 2  |-  ( -. 
{ A }  =  (/)  <->  A  e.  _V )
65con1bii 337 1  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 189    = wceq 1455   E.wex 1674    e. wcel 1898   _Vcvv 3057   (/)c0 3743   {csn 3980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-v 3059  df-dif 3419  df-nul 3744  df-sn 3981
This theorem is referenced by:  snnzb  4049  rabsnif  4054  prprc1  4095  prprc  4097  unisn2  4555  snexALT  4606  snex  4658  posn  4925  frsn  4927  relimasn  5213  elimasni  5217  inisegn0  5222  dmsnsnsn  5337  sucprc  5521  dffv3  5888  fconst5  6151  1stval  6827  2ndval  6828  ecexr  7399  snfi  7681  domunsn  7753  snnen2o  7792  hashrabrsn  12589  hashrabsn01  12590  hashrabsn1  12591  elprchashprn2  12611  hashsnlei  12631  hash2pwpr  12674  efgrelexlema  17454  usgra1v  25173  cusgra1v  25245  1conngra  25459  eldm3  30452  opelco3  30470  fvsingle  30737  unisnif  30742  funpartlem  30759  bj-sngltag  31623  wopprc  35931  usgr1v  39476  1conngr  40031
  Copyright terms: Public domain W3C validator