Theorem snexg 4229

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

Step	Hyp	Ref	Expression
1		pwexg 4225	. 2 |- ( A e. V -> ~P A e. _V )
2		snsspw 3805	. . 3 |- { A } C_ ~P A
3		ssexg 4184	. . 3 |- ( ( { A } C_ ~P A /\ ~P A e. _V ) -> { A } e. _V )
4	2, 3	mpan 424	. 2 |- ( ~P A e. _V -> { A } e. _V )
5	1, 4	syl 14	1 |- ( A e. V -> { A } e. _V )

Syntax hints:   -> wi 4   e. wcel 2176   _Vcvv 2772   C_ wss 3166   ~Pcpw 3616   {csn 3633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639

This theorem is referenced by:  snex  4230  notnotsnex  4232  exmidsssnc  4248  snelpwi  4257  opexg  4273  opm  4279  tpexg  4492  op1stbg  4527  sucexb  4546  elxp4  5171  elxp5  5172  opabex3d  6208  opabex3  6209  1stvalg  6230  2ndvalg  6231  mpoexxg  6298  cnvf1o  6313  brtpos2  6339  tfr0dm  6410  tfrlemisucaccv  6413  tfrlemibxssdm  6415  tfrlemibfn  6416  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  fvdiagfn  6782  ixpsnf1o  6825  mapsnf1o  6826  xpsnen2g  6926  zfz1isolem1  10987  climconst2  11635  ennnfonelemp1  12810  setsvalg  12895  setsex  12897  setsslid  12916  strle1g  12971  1strbas  12982  pwsval  13156  pwsbas  13157  pwssnf1o  13163  imasex  13170  imasival  13171  imasbas  13172  imasplusg  13173  imasmulr  13174  mgm1  13235  igsumvalx  13254  sgrp1  13276  mnd1  13320  mnd1id  13321  grp1  13471  grp1inv  13472  mulgnngsum  13496  triv1nsgd  13587  ring1  13854  znval  14431  znle  14432  znbaslemnn  14434  znbas  14439  znzrhval  14442  znzrhfo  14443  psrval  14461  psrbasg  14469  psrplusgg  14473