Theorem snexg 4202

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

Syntax hints:   → wi 4   ∈ wcel 2160  Vcvv 2752   ⊆ wss 3144  𝒫 cpw 3590  {csn 3607

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613

This theorem is referenced by:  snex  4203  notnotsnex  4205  exmidsssnc  4221  snelpwi  4230  opexg  4246  opm  4252  tpexg  4462  op1stbg  4497  sucexb  4514  elxp4  5134  elxp5  5135  opabex3d  6146  opabex3  6147  1stvalg  6167  2ndvalg  6168  mpoexxg  6235  cnvf1o  6250  brtpos2  6276  tfr0dm  6347  tfrlemisucaccv  6350  tfrlemibxssdm  6352  tfrlemibfn  6353  tfr1onlemsucaccv  6366  tfr1onlembxssdm  6368  tfr1onlembfn  6369  tfrcllemsucaccv  6379  tfrcllembxssdm  6381  tfrcllembfn  6382  fvdiagfn  6719  ixpsnf1o  6762  mapsnf1o  6763  xpsnen2g  6855  zfz1isolem1  10852  climconst2  11331  ennnfonelemp1  12457  setsvalg  12542  setsex  12544  setsslid  12563  strle1g  12618  1strbas  12629  imasex  12782  imasival  12783  imasbas  12784  imasplusg  12785  imasmulr  12786  mgm1  12846  sgrp1  12874  mnd1  12907  mnd1id  12908  grp1  13050  grp1inv  13051  triv1nsgd  13157  ring1  13411  znval  13932  znle  13933  znbaslemnn  13935  znbas  13939  psrval  13944  psrbasg  13951