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

Theorem snexALT 4154
Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, but proved using only Extensionality, Power Set, and Separation. Unlike the proof of zfpair 4170, Replacement is not needed. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) See also snex 4174. (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
snexALT  |-  { A }  e.  _V

Proof of Theorem snexALT
StepHypRef Expression
1 snsspw 3744 . . 3  |-  { A }  C_  ~P A
2 ssexg 4120 . . 3  |-  ( ( { A }  C_  ~P A  /\  ~P A  e.  _V )  ->  { A }  e.  _V )
31, 2mpan 654 . 2  |-  ( ~P A  e.  _V  ->  { A }  e.  _V )
4 pwexg 4152 . . . 4  |-  ( A  e.  _V  ->  ~P A  e.  _V )
54con3i 129 . . 3  |-  ( -. 
~P A  e.  _V  ->  -.  A  e.  _V )
6 snprc 3655 . . . . 5  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
76biimpi 188 . . . 4  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
8 0ex 4110 . . . 4  |-  (/)  e.  _V
97, 8syl6eqel 2344 . . 3  |-  ( -.  A  e.  _V  ->  { A }  e.  _V )
105, 9syl 17 . 2  |-  ( -. 
~P A  e.  _V  ->  { A }  e.  _V )
113, 10pm2.61i 158 1  |-  { A }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 5    = wceq 1619    e. wcel 1621   _Vcvv 2757    C_ wss 3113   (/)c0 3416   ~Pcpw 3585   {csn 3600
This theorem is referenced by:  p0exALT  4156  dfiota3  23823  brsuccf  23841  funpartfun  23842  funpartfv  23844  smbkle  25396  cndpv  25402  pgapspf  25405  lineval222  25432  lineval3a  25436  sgplpte21  25485  sgplpte22  25491  isray2  25506  isray  25507
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pow 4146
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-v 2759  df-dif 3116  df-in 3120  df-ss 3127  df-nul 3417  df-pw 3587  df-sn 3606
  Copyright terms: Public domain W3C validator