Theorem snexg 4323

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 4319	. 2 |- ( A e. V -> ~P A e. _V )
2		snsspw 3889	. . 3 |- { A } C_ ~P A
3		ssexg 4274	. . 3 |- ( ( { A } C_ ~P A /\ ~P A e. _V ) -> { A } e. _V )
4	2, 3	mpan 428	. 2 |- ( ~P A e. _V -> { A } e. _V )
5	1, 4	syl 14	1 |- ( A e. V -> { A } e. _V )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   _Vcvv 2821   C_ wss 3220   ~Pcpw 3688   {csn 3709

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715

This theorem is used by:  snex  4324  notnotsnex  4326  exmidsssnc  4342  snelpwg  4352  snelpwi  4353  opexg  4370  opm  4376  tpexg  4592  op1stbg  4627  sucexb  4646  elxp4  5278  elxp5  5279  opabex3d  6354  opabex3  6355  1stvalg  6380  2ndvalg  6381  mpoexxg  6450  cnvf1o  6465  suppsnopdc  6494  brtpos2  6526  tfr0dm  6597  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemibfn  6603  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  mapsnd  6974  fvdiagfn  6979  ixpsnf1o  7022  mapsnf1o  7023  mapsnend  7103  xpsnen2g  7131  fczfsuppd  7302  snopfsuppdc  7304  zfz1isolem1  11314  climconst2  12082  ennnfonelemp1  13355  setsvalg  13440  setsex  13442  setsslid  13461  strle1g  13519  1strbas  13530  imasex  13685  imasival  13686  imasbas  13687  imasplusg  13688  imasmulr  13689  mgm1  13749  gzsumvalx  13768  sgrp1  13785  mnd1  13821  mnd1id  13822  grp1  13970  grp1inv  13971  mulgnngzsum  13989  triv1nsgd  14080  pwsval  14311  pwsbas  14312  pwssnf1o  14318  ring1  14471  znval  15080  znle  15081  znbaslemnn  15083  znbas  15088  znzrhval  15091  znzrhfo  15092  psrval  15159  psrbasg  15178  psrplusgg  15182  psrmulrg  15186  upgr1eopdc  16569  upgr1een  16570  umgr1een  16571  uspgr1eopdc  16689  usgr1eop  16691  1loopgrvd2fi  16751  1loopgrvd0fi  16752  p1evtxdeqfilem  16757  p1evtxdeqfi  16758  p1evtxdp1fi  16759  eupth2lem3fi  16922