Theorem snexg 4170

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

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 2730   ⊆ wss 3121  𝒫 cpw 3566  {csn 3583

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589

This theorem is referenced by:  snex  4171  notnotsnex  4173  exmidsssnc  4189  snelpwi  4197  opexg  4213  opm  4219  tpexg  4429  op1stbg  4464  sucexb  4481  elxp4  5098  elxp5  5099  opabex3d  6100  opabex3  6101  1stvalg  6121  2ndvalg  6122  mpoexxg  6189  cnvf1o  6204  brtpos2  6230  tfr0dm  6301  tfrlemisucaccv  6304  tfrlemibxssdm  6306  tfrlemibfn  6307  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  fvdiagfn  6671  ixpsnf1o  6714  mapsnf1o  6715  xpsnen2g  6807  zfz1isolem1  10775  climconst2  11254  ennnfonelemp1  12361  setsvalg  12446  setsex  12448  setsslid  12466  strle1g  12508  1strbas  12517  mgm1  12624  sgrp1  12651  mnd1  12679  mnd1id  12680