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  11292  climconst2  12057  ennnfonelemp1  13297  setsvalg  13382  setsex  13384  setsslid  13403  strle1g  13460  1strbas  13471  imasex  13626  imasival  13627  imasbas  13628  imasplusg  13629  imasmulr  13630  mgm1  13690  gzsumvalx  13709  sgrp1  13726  mnd1  13762  mnd1id  13763  grp1  13911  grp1inv  13912  mulgnngzsum  13930  triv1nsgd  14021  pwsval  14204  pwsbas  14205  pwssnf1o  14211  ring1  14364  znval  14971  znle  14972  znbaslemnn  14974  znbas  14979  znzrhval  14982  znzrhfo  14983  psrval  15050  psrbasg  15065  psrplusgg  15069  upgr1eopdc  16364  upgr1een  16365  umgr1een  16366  uspgr1eopdc  16484  usgr1eop  16486  1loopgrvd2fi  16546  1loopgrvd0fi  16547  p1evtxdeqfilem  16552  p1evtxdeqfi  16553  p1evtxdp1fi  16554  eupth2lem3fi  16717