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

Theorem snexALT 4195
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 4211, Replacement is not needed. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) See also snex 4215. (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
snexALT  |-  { A }  e.  _V

Proof of Theorem snexALT
StepHypRef Expression
1 snsspw 3785 . . 3  |-  { A }  C_  ~P A
2 ssexg 4161 . . 3  |-  ( ( { A }  C_  ~P A  /\  ~P A  e.  _V )  ->  { A }  e.  _V )
31, 2mpan 651 . 2  |-  ( ~P A  e.  _V  ->  { A }  e.  _V )
4 pwexg 4193 . . . 4  |-  ( A  e.  _V  ->  ~P A  e.  _V )
54con3i 127 . . 3  |-  ( -. 
~P A  e.  _V  ->  -.  A  e.  _V )
6 snprc 3696 . . . . 5  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
76biimpi 186 . . . 4  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
8 0ex 4151 . . . 4  |-  (/)  e.  _V
97, 8syl6eqel 2372 . . 3  |-  ( -.  A  e.  _V  ->  { A }  e.  _V )
105, 9syl 15 . 2  |-  ( -. 
~P A  e.  _V  ->  { A }  e.  _V )
113, 10pm2.61i 156 1  |-  { A }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1623    e. wcel 1685   _Vcvv 2789    C_ wss 3153   (/)c0 3456   ~Pcpw 3626   {csn 3641
This theorem is referenced by:  p0exALT  4197  dfiota3  23872  brsuccf  23890  funpartfun  23891  funpartfv  23893  smbkle  25454  cndpv  25460  pgapspf  25463  lineval222  25490  lineval3a  25494  sgplpte21  25543  sgplpte22  25549  isray2  25564  isray  25565
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-v 2791  df-dif 3156  df-in 3160  df-ss 3167  df-nul 3457  df-pw 3628  df-sn 3647
  Copyright terms: Public domain W3C validator