Theorem snexg 4228

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

Syntax hints:   → wi 4   ∈ wcel 2176  Vcvv 2772   ⊆ wss 3166  𝒫 cpw 3616  {csn 3633

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639

This theorem is referenced by:  snex  4229  notnotsnex  4231  exmidsssnc  4247  snelpwi  4256  opexg  4272  opm  4278  tpexg  4491  op1stbg  4526  sucexb  4545  elxp4  5170  elxp5  5171  opabex3d  6206  opabex3  6207  1stvalg  6228  2ndvalg  6229  mpoexxg  6296  cnvf1o  6311  brtpos2  6337  tfr0dm  6408  tfrlemisucaccv  6411  tfrlemibxssdm  6413  tfrlemibfn  6414  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  fvdiagfn  6780  ixpsnf1o  6823  mapsnf1o  6824  xpsnen2g  6924  zfz1isolem1  10985  climconst2  11602  ennnfonelemp1  12777  setsvalg  12862  setsex  12864  setsslid  12883  strle1g  12938  1strbas  12949  pwsval  13123  pwsbas  13124  pwssnf1o  13130  imasex  13137  imasival  13138  imasbas  13139  imasplusg  13140  imasmulr  13141  mgm1  13202  igsumvalx  13221  sgrp1  13243  mnd1  13287  mnd1id  13288  grp1  13438  grp1inv  13439  mulgnngsum  13463  triv1nsgd  13554  ring1  13821  znval  14398  znle  14399  znbaslemnn  14401  znbas  14406  znzrhval  14409  znzrhfo  14410  psrval  14428  psrbasg  14436  psrplusgg  14440