Theorem snexg 4171

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 4167	. 2 |- ( A e. V -> ~P A e. _V )
2		snsspw 3752	. . 3 |- { A } C_ ~P A
3		ssexg 4129	. . 3 |- ( ( { A } C_ ~P A /\ ~P A e. _V ) -> { A } e. _V )
4	2, 3	mpan 422	. 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 2142   _Vcvv 2731   C_ wss 3122   ~Pcpw 3567   {csn 3584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-pow 4161

This theorem depends on definitions:  df-bi 116  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-v 2733  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590

This theorem is referenced by:  snex  4172  notnotsnex  4174  exmidsssnc  4190  snelpwi  4198  opexg  4214  opm  4220  tpexg  4430  op1stbg  4465  sucexb  4482  elxp4  5100  elxp5  5101  opabex3d  6104  opabex3  6105  1stvalg  6125  2ndvalg  6126  mpoexxg  6193  cnvf1o  6208  brtpos2  6234  tfr0dm  6305  tfrlemisucaccv  6308  tfrlemibxssdm  6310  tfrlemibfn  6311  tfr1onlemsucaccv  6324  tfr1onlembxssdm  6326  tfr1onlembfn  6327  tfrcllemsucaccv  6337  tfrcllembxssdm  6339  tfrcllembfn  6340  fvdiagfn  6675  ixpsnf1o  6718  mapsnf1o  6719  xpsnen2g  6811  zfz1isolem1  10779  climconst2  11258  ennnfonelemp1  12365  setsvalg  12450  setsex  12452  setsslid  12470  strle1g  12512  1strbas  12521  mgm1  12628  sgrp1  12655  mnd1  12683  mnd1id  12684  grp1  12809  grp1inv  12810