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

Theorem snprc 3858
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 3816 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21exbii 1592 . . 3  |-  ( E. x  x  e.  { A }  <->  E. x  x  =  A )
3 neq0 3625 . . 3  |-  ( -. 
{ A }  =  (/)  <->  E. x  x  e.  { A } )
4 isset 2947 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
52, 3, 43bitr4i 269 . 2  |-  ( -. 
{ A }  =  (/)  <->  A  e.  _V )
65con1bii 322 1  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177   E.wex 1550    = wceq 1652    e. wcel 1725   _Vcvv 2943   (/)c0 3615   {csn 3801
This theorem is referenced by:  rabrsn  3861  prprc1  3901  prprc  3903  snexALT  4372  snex  4392  sucprc  4643  unisn2  4697  posn  4932  frsn  4934  relimasn  5213  elimasni  5217  dmsnsnsn  5334  dffv3  5710  fconst5  5935  1stval  6337  2ndval  6338  ecexr  6896  snfi  7173  domunsn  7243  hashrabrsn  11631  elprchashprn2  11650  hashsnlei  11663  efgrelexlema  15364  usgra1v  21392  cusgra1v  21453  1conngra  21645  eldm3  25369  fvsingle  25710  unisnif  25715  funpartlem  25732  wopprc  27033  inisegn0  27050
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-v 2945  df-dif 3310  df-nul 3616  df-sn 3807
  Copyright terms: Public domain W3C validator