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

Theorem snprc 3696
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 }  =  (/) )
Dummy variable  x is distinct from all other variables.

Proof of Theorem snprc
StepHypRef Expression
1 elsn 3656 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21exbii 1570 . . 3  |-  ( E. x  x  e.  { A }  <->  E. x  x  =  A )
3 neq0 3466 . . 3  |-  ( -. 
{ A }  =  (/)  <->  E. x  x  e.  { A } )
4 isset 2793 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
52, 3, 43bitr4i 270 . 2  |-  ( -. 
{ A }  =  (/)  <->  A  e.  _V )
65con1bii 323 1  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    <-> wb 178   E.wex 1529    = wceq 1624    e. wcel 1685   _Vcvv 2789   (/)c0 3456   {csn 3641
This theorem is referenced by:  prprc1  3737  prprc  3739  snexALT  4195  snex  4215  sucprc  4466  unisn2  4521  posn  4757  frsn  4759  relimasn  5035  elimasni  5039  dmsnsnsn  5149  fv2  5481  fvprc  5482  fconst5  5692  1stval  6085  2ndval  6086  ecexr  6660  snfi  6936  domunsn  7006  hashsnlei  11370  efgrelexlema  15052  unisnif  23871  funpartfv  23890  wopprc  26522  inisegn0  26539
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-v 2791  df-dif 3156  df-nul 3457  df-sn 3647
  Copyright terms: Public domain W3C validator