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

Theorem snprc 4037
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 3988 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21exbii 1690 . . 3  |-  ( E. x  x  e.  { A }  <->  E. x  x  =  A )
3 neq0 3751 . . 3  |-  ( -. 
{ A }  =  (/)  <->  E. x  x  e.  { A } )
4 isset 3065 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
52, 3, 43bitr4i 279 . 2  |-  ( -. 
{ A }  =  (/)  <->  A  e.  _V )
65con1bii 331 1  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 186    = wceq 1407   E.wex 1635    e. wcel 1844   _Vcvv 3061   (/)c0 3740   {csn 3974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-v 3063  df-dif 3419  df-nul 3741  df-sn 3975
This theorem is referenced by:  snnzb  4038  rabsnif  4043  prprc1  4084  prprc  4086  unisn2  4532  snexALT  4582  snex  4634  posn  4894  frsn  4896  relimasn  5182  elimasni  5186  dmsnsnsn  5304  sucprc  5487  dffv3  5847  fconst5  6111  1stval  6788  2ndval  6789  ecexr  7355  snfi  7636  domunsn  7707  snnen2o  7746  hashrabrsn  12490  hashrabsn01  12491  hashrabsn1  12492  elprchashprn2  12512  hashsnlei  12529  hash2pwpr  12570  efgrelexlema  17093  usgra1v  24819  cusgra1v  24890  1conngra  25104  eldm3  29988  opelco3  30006  fvsingle  30271  unisnif  30276  funpartlem  30293  bj-sngltag  31119  wopprc  35347  inisegn0  35364
  Copyright terms: Public domain W3C validator