Theorem snexg 3983

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

Syntax hints:   → wi 4   ∈ wcel 1434  Vcvv 2612   ⊆ wss 2984  𝒫 cpw 3406  {csn 3422

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-v 2614  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428

This theorem is referenced by:  snex  3984  notnotsnex  3986  snelpwi  4003  opexg  4019  opm  4025  tpexg  4233  op1stbg  4264  sucexb  4277  elxp4  4872  elxp5  4873  opabex3d  5827  opabex3  5828  1stvalg  5848  2ndvalg  5849  mpt2exxg  5912  cnvf1o  5925  brtpos2  5948  tfr0dm  6019  tfrlemisucaccv  6022  tfrlemibxssdm  6024  tfrlemibfn  6025  tfr1onlemsucaccv  6038  tfr1onlembxssdm  6040  tfr1onlembfn  6041  tfrcllemsucaccv  6051  tfrcllembxssdm  6053  tfrcllembfn  6054  fvdiagfn  6380  xpsnen2g  6475  climconst2  10504