ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  snexg Unicode version

Theorem snexg 3983
Description: A singleton whose element exists is a set. The  A  e.  _V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.)
Assertion
Ref Expression
snexg  |-  ( A  e.  V  ->  { A }  e.  _V )

Proof of Theorem snexg
StepHypRef Expression
1 pwexg 3980 . 2  |-  ( A  e.  V  ->  ~P A  e.  _V )
2 snsspw 3582 . . 3  |-  { A }  C_  ~P A
3 ssexg 3943 . . 3  |-  ( ( { A }  C_  ~P A  /\  ~P A  e.  _V )  ->  { A }  e.  _V )
42, 3mpan 415 . 2  |-  ( ~P A  e.  _V  ->  { A }  e.  _V )
51, 4syl 14 1  |-  ( A  e.  V  ->  { A }  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   _Vcvv 2612    C_ wss 2984   ~Pcpw 3406   {csn 3422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-v 2614  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428
This theorem is referenced by:  snex  3984  notnotsnex  3986  snelpwi  4003  opexg  4019  opm  4025  tpexg  4233  op1stbg  4264  sucexb  4277  elxp4  4872  elxp5  4873  opabex3d  5827  opabex3  5828  1stvalg  5848  2ndvalg  5849  mpt2exxg  5912  cnvf1o  5925  brtpos2  5948  tfr0dm  6019  tfrlemisucaccv  6022  tfrlemibxssdm  6024  tfrlemibfn  6025  tfr1onlemsucaccv  6038  tfr1onlembxssdm  6040  tfr1onlembfn  6041  tfrcllemsucaccv  6051  tfrcllembxssdm  6053  tfrcllembfn  6054  fvdiagfn  6380  xpsnen2g  6475  climconst2  10504
  Copyright terms: Public domain W3C validator