Theorem snexg 4244

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

Syntax hints:   → wi 4   ∈ wcel 2178  Vcvv 2776   ⊆ wss 3174  𝒫 cpw 3626  {csn 3643

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649

This theorem is referenced by:  snex  4245  notnotsnex  4247  exmidsssnc  4263  snelpwg  4272  snelpwi  4273  opexg  4290  opm  4296  tpexg  4509  op1stbg  4544  sucexb  4563  elxp4  5189  elxp5  5190  opabex3d  6229  opabex3  6230  1stvalg  6251  2ndvalg  6252  mpoexxg  6319  cnvf1o  6334  brtpos2  6360  tfr0dm  6431  tfrlemisucaccv  6434  tfrlemibxssdm  6436  tfrlemibfn  6437  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  fvdiagfn  6803  ixpsnf1o  6846  mapsnf1o  6847  xpsnen2g  6949  zfz1isolem1  11022  climconst2  11717  ennnfonelemp1  12892  setsvalg  12977  setsex  12979  setsslid  12998  strle1g  13053  1strbas  13064  pwsval  13238  pwsbas  13239  pwssnf1o  13245  imasex  13252  imasival  13253  imasbas  13254  imasplusg  13255  imasmulr  13256  mgm1  13317  igsumvalx  13336  sgrp1  13358  mnd1  13402  mnd1id  13403  grp1  13553  grp1inv  13554  mulgnngsum  13578  triv1nsgd  13669  ring1  13936  znval  14513  znle  14514  znbaslemnn  14516  znbas  14521  znzrhval  14524  znzrhfo  14525  psrval  14543  psrbasg  14551  psrplusgg  14555  upgr1eopdc  15831