Theorem snexg 4302

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

Syntax hints:   → wi 4   ∈ wcel 2205  Vcvv 2815   ⊆ wss 3214  𝒫 cpw 3674  {csn 3694

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700

This theorem is referenced by:  snex  4303  notnotsnex  4305  exmidsssnc  4321  snelpwg  4331  snelpwi  4332  opexg  4349  opm  4355  tpexg  4570  op1stbg  4605  sucexb  4624  elxp4  5255  elxp5  5256  opabex3d  6323  opabex3  6324  1stvalg  6349  2ndvalg  6350  mpoexxg  6419  cnvf1o  6434  suppsnopdc  6463  brtpos2  6495  tfr0dm  6566  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemibfn  6572  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  mapsnd  6936  fvdiagfn  6941  ixpsnf1o  6984  mapsnf1o  6985  mapsnend  7065  xpsnen2g  7093  fczfsuppd  7263  snopfsuppdc  7265  zfz1isolem1  11237  climconst2  12001  ennnfonelemp1  13241  setsvalg  13326  setsex  13328  setsslid  13347  strle1g  13403  1strbas  13414  imasex  13569  imasival  13570  imasbas  13571  imasplusg  13572  imasmulr  13573  mgm1  13633  igsumvalx  13652  sgrp1  13674  mnd1  13710  mnd1id  13711  grp1  13861  grp1inv  13862  mulgnngsum  13880  triv1nsgd  13971  pwsval  14146  pwsbas  14147  pwssnf1o  14153  ring1  14302  znval  14910  znle  14911  znbaslemnn  14913  znbas  14918  znzrhval  14921  znzrhfo  14922  psrval  14940  psrbasg  14955  psrplusgg  14959  upgr1eopdc  16244  upgr1een  16245  umgr1een  16246  uspgr1eopdc  16364  usgr1eop  16366  1loopgrvd2fi  16426  1loopgrvd0fi  16427  p1evtxdeqfilem  16432  p1evtxdeqfi  16433  p1evtxdp1fi  16434  eupth2lem3fi  16597