Theorem snexg 4267

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

Syntax hints:   → wi 4   ∈ wcel 2200  Vcvv 2799   ⊆ wss 3197  𝒫 cpw 3649  {csn 3666

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672

This theorem is referenced by:  snex  4268  notnotsnex  4270  exmidsssnc  4286  snelpwg  4295  snelpwi  4296  opexg  4313  opm  4319  tpexg  4534  op1stbg  4569  sucexb  4588  elxp4  5215  elxp5  5216  opabex3d  6264  opabex3  6265  1stvalg  6286  2ndvalg  6287  mpoexxg  6354  cnvf1o  6369  brtpos2  6395  tfr0dm  6466  tfrlemisucaccv  6469  tfrlemibxssdm  6471  tfrlemibfn  6472  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllembfn  6501  fvdiagfn  6838  ixpsnf1o  6881  mapsnf1o  6882  xpsnen2g  6984  zfz1isolem1  11057  climconst2  11797  ennnfonelemp1  12972  setsvalg  13057  setsex  13059  setsslid  13078  strle1g  13134  1strbas  13145  pwsval  13319  pwsbas  13320  pwssnf1o  13326  imasex  13333  imasival  13334  imasbas  13335  imasplusg  13336  imasmulr  13337  mgm1  13398  igsumvalx  13417  sgrp1  13439  mnd1  13483  mnd1id  13484  grp1  13634  grp1inv  13635  mulgnngsum  13659  triv1nsgd  13750  ring1  14017  znval  14594  znle  14595  znbaslemnn  14597  znbas  14602  znzrhval  14605  znzrhfo  14606  psrval  14624  psrbasg  14632  psrplusgg  14636  upgr1eopdc  15917