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  6527  tfr0dm  6598  tfrlemisucaccv  6601  tfrlemibxssdm  6603  tfrlemibfn  6604  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  mapsnd  6976  fvdiagfn  6981  ixpsnf1o  7024  mapsnf1o  7025  mapsnend  7105  xpsnen2g  7133  fczfsuppd  7304  snopfsupp  7306  zfz1isolem1  11313  climconst2  12081  ennnfonelemp1  13354  setsvalg  13439  setsex  13441  setsslid  13460  strle1g  13518  1strbas  13529  imasex  13684  imasival  13685  imasbas  13686  imasplusg  13687  imasmulr  13688  mgm1  13748  gzsumvalx  13767  sgrp1  13784  mnd1  13820  mnd1id  13821  grp1  13969  grp1inv  13970  mulgnngzsum  13988  triv1nsgd  14079  pwsval  14310  pwsbas  14311  pwssnf1o  14317  ring1  14470  znval  15079  znle  15080  znbaslemnn  15082  znbas  15087  znzrhval  15090  znzrhfo  15091  psrval  15160  psrbasg  15187  psrplusgg  15191  psrmulrg  15195  upgr1eopdc  16586  upgr1een  16587  umgr1een  16588  uspgr1eopdc  16706  usgr1eop  16708  1loopgrvd2fi  16768  1loopgrvd0fi  16769  p1evtxdeqfilem  16774  p1evtxdeqfi  16775  p1evtxdp1fi  16776  eupth2lem3fi  16939