Theorem snexg 4217

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 4213	. 2 |- ( A e. V -> ~P A e. _V )
2		snsspw 3794	. . 3 |- { A } C_ ~P A
3		ssexg 4172	. . 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 2167   _Vcvv 2763   C_ wss 3157   ~Pcpw 3605   {csn 3622

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628

This theorem is referenced by:  snex  4218  notnotsnex  4220  exmidsssnc  4236  snelpwi  4245  opexg  4261  opm  4267  tpexg  4479  op1stbg  4514  sucexb  4533  elxp4  5157  elxp5  5158  opabex3d  6178  opabex3  6179  1stvalg  6200  2ndvalg  6201  mpoexxg  6268  cnvf1o  6283  brtpos2  6309  tfr0dm  6380  tfrlemisucaccv  6383  tfrlemibxssdm  6385  tfrlemibfn  6386  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  fvdiagfn  6752  ixpsnf1o  6795  mapsnf1o  6796  xpsnen2g  6888  zfz1isolem1  10932  climconst2  11456  ennnfonelemp1  12623  setsvalg  12708  setsex  12710  setsslid  12729  strle1g  12784  1strbas  12795  imasex  12948  imasival  12949  imasbas  12950  imasplusg  12951  imasmulr  12952  mgm1  13013  igsumvalx  13032  sgrp1  13054  mnd1  13087  mnd1id  13088  grp1  13238  grp1inv  13239  mulgnngsum  13257  triv1nsgd  13348  ring1  13615  znval  14192  znle  14193  znbaslemnn  14195  znbas  14200  znzrhval  14203  znzrhfo  14204  psrval  14220  psrbasg  14227  psrplusgg  14230