Theorem snexg 4321

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  Vcvv 2821   ⊆ wss 3220  𝒫 cpw 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 4249  ax-pow 4311

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  4322  notnotsnex  4324  exmidsssnc  4340  snelpwg  4350  snelpwi  4351  opexg  4368  opm  4374  tpexg  4590  op1stbg  4625  sucexb  4644  elxp4  5275  elxp5  5276  opabex3d  6350  opabex3  6351  1stvalg  6376  2ndvalg  6377  mpoexxg  6446  cnvf1o  6461  suppsnopdc  6490  brtpos2  6522  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  mapsnd  6970  fvdiagfn  6975  ixpsnf1o  7018  mapsnf1o  7019  mapsnend  7099  xpsnen2g  7127  fczfsuppd  7297  snopfsuppdc  7299  zfz1isolem1  11308  climconst2  12076  ennnfonelemp1  13349  setsvalg  13434  setsex  13436  setsslid  13455  strle1g  13513  1strbas  13524  imasex  13679  imasival  13680  imasbas  13681  imasplusg  13682  imasmulr  13683  mgm1  13743  gzsumvalx  13762  sgrp1  13779  mnd1  13815  mnd1id  13816  grp1  13964  grp1inv  13965  mulgnngzsum  13983  triv1nsgd  14074  pwsval  14288  pwsbas  14289  pwssnf1o  14295  ring1  14448  znval  15055  znle  15056  znbaslemnn  15058  znbas  15063  znzrhval  15066  znzrhfo  15067  psrval  15134  psrbasg  15150  psrplusgg  15154  psrmulrg  15158  upgr1eopdc  16530  upgr1een  16531  umgr1een  16532  uspgr1eopdc  16650  usgr1eop  16652  1loopgrvd2fi  16712  1loopgrvd0fi  16713  p1evtxdeqfilem  16718  p1evtxdeqfi  16719  p1evtxdp1fi  16720  eupth2lem3fi  16883