Theorem snexg 4316

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 4312	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
2		snsspw 3884	. . 3 ⊢ {𝐴} ⊆ 𝒫 𝐴
3		ssexg 4267	. . 3 ⊢ (({𝐴} ⊆ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ V) → {𝐴} ∈ V)
4	2, 3	mpan 428	. 2 ⊢ (𝒫 𝐴 ∈ V → {𝐴} ∈ V)
5	1, 4	syl 14	1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2209  Vcvv 2821   ⊆ wss 3220  𝒫 cpw 3685  {csn 3705

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 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 4244  ax-pow 4306

This theorem 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 3687  df-sn 3711

This theorem is referenced by:  snex  4317  notnotsnex  4319  exmidsssnc  4335  snelpwg  4345  snelpwi  4346  opexg  4363  opm  4369  tpexg  4585  op1stbg  4620  sucexb  4639  elxp4  5270  elxp5  5271  opabex3d  6340  opabex3  6341  1stvalg  6366  2ndvalg  6367  mpoexxg  6436  cnvf1o  6451  suppsnopdc  6480  brtpos2  6512  tfr0dm  6583  tfrlemisucaccv  6586  tfrlemibxssdm  6588  tfrlemibfn  6589  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  mapsnd  6960  fvdiagfn  6965  ixpsnf1o  7008  mapsnf1o  7009  mapsnend  7089  xpsnen2g  7117  fczfsuppd  7287  snopfsuppdc  7289  zfz1isolem1  11270  climconst2  12035  ennnfonelemp1  13275  setsvalg  13360  setsex  13362  setsslid  13381  strle1g  13437  1strbas  13448  imasex  13603  imasival  13604  imasbas  13605  imasplusg  13606  imasmulr  13607  mgm1  13667  gzsumvalx  13686  sgrp1  13703  mnd1  13739  mnd1id  13740  grp1  13888  grp1inv  13889  mulgnngzsum  13907  triv1nsgd  13998  pwsval  14181  pwsbas  14182  pwssnf1o  14188  ring1  14337  znval  14943  znle  14944  znbaslemnn  14946  znbas  14951  znzrhval  14954  znzrhfo  14955  psrval  14973  psrbasg  14988  psrplusgg  14992  upgr1eopdc  16278  upgr1een  16279  umgr1een  16280  uspgr1eopdc  16398  usgr1eop  16400  1loopgrvd2fi  16460  1loopgrvd0fi  16461  p1evtxdeqfilem  16466  p1evtxdeqfi  16467  p1evtxdp1fi  16468  eupth2lem3fi  16631