Theorem snexg 4245

Description: A singleton whose element exists is a set. The 𝐴 ∈ 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	⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)

Proof of Theorem snexg

Step	Hyp	Ref	Expression
1		pwexg 4241	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
2		snsspw 3819	. . 3 ⊢ {𝐴} ⊆ 𝒫 𝐴
3		ssexg 4200	. . 3 ⊢ (({𝐴} ⊆ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ V) → {𝐴} ∈ V)
4	2, 3	mpan 424	. 2 ⊢ (𝒫 𝐴 ∈ V → {𝐴} ∈ V)
5	1, 4	syl 14	1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2178  Vcvv 2777   ⊆ wss 3175  𝒫 cpw 3627  {csn 3644

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4179  ax-pow 4235

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2779  df-in 3181  df-ss 3188  df-pw 3629  df-sn 3650

This theorem is referenced by:  snex  4246  notnotsnex  4248  exmidsssnc  4264  snelpwg  4273  snelpwi  4274  opexg  4291  opm  4297  tpexg  4510  op1stbg  4545  sucexb  4564  elxp4  5190  elxp5  5191  opabex3d  6231  opabex3  6232  1stvalg  6253  2ndvalg  6254  mpoexxg  6321  cnvf1o  6336  brtpos2  6362  tfr0dm  6433  tfrlemisucaccv  6436  tfrlemibxssdm  6438  tfrlemibfn  6439  tfr1onlemsucaccv  6452  tfr1onlembxssdm  6454  tfr1onlembfn  6455  tfrcllemsucaccv  6465  tfrcllembxssdm  6467  tfrcllembfn  6468  fvdiagfn  6805  ixpsnf1o  6848  mapsnf1o  6849  xpsnen2g  6951  zfz1isolem1  11024  climconst2  11763  ennnfonelemp1  12938  setsvalg  13023  setsex  13025  setsslid  13044  strle1g  13099  1strbas  13110  pwsval  13284  pwsbas  13285  pwssnf1o  13291  imasex  13298  imasival  13299  imasbas  13300  imasplusg  13301  imasmulr  13302  mgm1  13363  igsumvalx  13382  sgrp1  13404  mnd1  13448  mnd1id  13449  grp1  13599  grp1inv  13600  mulgnngsum  13624  triv1nsgd  13715  ring1  13982  znval  14559  znle  14560  znbaslemnn  14562  znbas  14567  znzrhval  14570  znzrhfo  14571  psrval  14589  psrbasg  14597  psrplusgg  14601  upgr1eopdc  15880