Theorem snexg 4116

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

Syntax hints:   → wi 4   ∈ wcel 1481  Vcvv 2689   ⊆ wss 3076  𝒫 cpw 3515  {csn 3532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538

This theorem is referenced by:  snex  4117  notnotsnex  4119  exmidsssnc  4134  snelpwi  4142  opexg  4158  opm  4164  tpexg  4373  op1stbg  4408  sucexb  4421  elxp4  5034  elxp5  5035  opabex3d  6027  opabex3  6028  1stvalg  6048  2ndvalg  6049  mpoexxg  6116  cnvf1o  6130  brtpos2  6156  tfr0dm  6227  tfrlemisucaccv  6230  tfrlemibxssdm  6232  tfrlemibfn  6233  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  fvdiagfn  6595  ixpsnf1o  6638  mapsnf1o  6639  xpsnen2g  6731  zfz1isolem1  10615  climconst2  11092  ennnfonelemp1  11955  setsvalg  12028  setsex  12030  setsslid  12048  strle1g  12088  1strbas  12097