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  11306  climconst2  12073  ennnfonelemp1  13346  setsvalg  13431  setsex  13433  setsslid  13452  strle1g  13509  1strbas  13520  imasex  13675  imasival  13676  imasbas  13677  imasplusg  13678  imasmulr  13679  mgm1  13739  gzsumvalx  13758  sgrp1  13775  mnd1  13811  mnd1id  13812  grp1  13960  grp1inv  13961  mulgnngzsum  13979  triv1nsgd  14070  pwsval  14253  pwsbas  14254  pwssnf1o  14260  ring1  14413  znval  15020  znle  15021  znbaslemnn  15023  znbas  15028  znzrhval  15031  znzrhfo  15032  psrval  15099  psrbasg  15114  psrplusgg  15118  upgr1eopdc  16462  upgr1een  16463  umgr1een  16464  uspgr1eopdc  16582  usgr1eop  16584  1loopgrvd2fi  16644  1loopgrvd0fi  16645  p1evtxdeqfilem  16650  p1evtxdeqfi  16651  p1evtxdp1fi  16652  eupth2lem3fi  16815