Theorem snexg 4272

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 4268	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
2		snsspw 3845	. . 3 ⊢ {𝐴} ⊆ 𝒫 𝐴
3		ssexg 4226	. . 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 2800   ⊆ wss 3198  𝒫 cpw 3650  {csn 3667

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 4205  ax-pow 4262

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 2802  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673

This theorem is referenced by:  snex  4273  notnotsnex  4275  exmidsssnc  4291  snelpwg  4300  snelpwi  4301  opexg  4318  opm  4324  tpexg  4539  op1stbg  4574  sucexb  4593  elxp4  5222  elxp5  5223  opabex3d  6278  opabex3  6279  1stvalg  6300  2ndvalg  6301  mpoexxg  6370  cnvf1o  6385  brtpos2  6412  tfr0dm  6483  tfrlemisucaccv  6486  tfrlemibxssdm  6488  tfrlemibfn  6489  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  fvdiagfn  6857  ixpsnf1o  6900  mapsnf1o  6901  xpsnen2g  7008  zfz1isolem1  11094  climconst2  11842  ennnfonelemp1  13017  setsvalg  13102  setsex  13104  setsslid  13123  strle1g  13179  1strbas  13190  pwsval  13364  pwsbas  13365  pwssnf1o  13371  imasex  13378  imasival  13379  imasbas  13380  imasplusg  13381  imasmulr  13382  mgm1  13443  igsumvalx  13462  sgrp1  13484  mnd1  13528  mnd1id  13529  grp1  13679  grp1inv  13680  mulgnngsum  13704  triv1nsgd  13795  ring1  14062  znval  14640  znle  14641  znbaslemnn  14643  znbas  14648  znzrhval  14651  znzrhfo  14652  psrval  14670  psrbasg  14678  psrplusgg  14682  upgr1eopdc  15964  uspgr1eopdc  16082  usgr1eop  16084  1loopgrvd2fi  16111  1loopgrvd0fi  16112