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

Theorem snexg 3963
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 3960 . 2  |-  ( A  e.  V  ->  ~P A  e.  _V )
2 snsspw 3562 . . 3  |-  { A }  C_  ~P A
3 ssexg 3923 . . 3  |-  ( ( { A }  C_  ~P A  /\  ~P A  e.  _V )  ->  { A }  e.  _V )
42, 3mpan 408 . 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 1409   _Vcvv 2574    C_ wss 2944   ~Pcpw 3386   {csn 3402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408
This theorem is referenced by:  snex  3964  opexg  3991  tpexg  4206  opabex3d  5775  opabex3  5776  mpt2exxg  5860  cnvf1o  5873  brtpos2  5896  tfr0  5967  tfrlemisucaccv  5969  tfrlemibxssdm  5971  tfrlemibfn  5972  xpsnen2g  6333  iseqid3  9403  climconst2  10035
  Copyright terms: Public domain W3C validator