Theorem snexg 4297

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

Syntax hints:   → wi 4   ∈ wcel 2203  Vcvv 2813   ⊆ wss 3211  𝒫 cpw 3669  {csn 3689

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695

This theorem is referenced by:  snex  4298  notnotsnex  4300  exmidsssnc  4316  snelpwg  4326  snelpwi  4327  opexg  4344  opm  4350  tpexg  4565  op1stbg  4600  sucexb  4619  elxp4  5250  elxp5  5251  opabex3d  6314  opabex3  6315  1stvalg  6336  2ndvalg  6337  mpoexxg  6406  cnvf1o  6421  suppsnopdc  6450  brtpos2  6482  tfr0dm  6553  tfrlemisucaccv  6556  tfrlemibxssdm  6558  tfrlemibfn  6559  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  mapsnd  6923  fvdiagfn  6928  ixpsnf1o  6971  mapsnf1o  6972  mapsnend  7052  xpsnen2g  7080  fczfsuppd  7250  snopfsuppdc  7252  zfz1isolem1  11212  climconst2  11976  ennnfonelemp1  13157  setsvalg  13242  setsex  13244  setsslid  13263  strle1g  13319  1strbas  13330  pwsval  13504  pwsbas  13505  pwssnf1o  13511  imasex  13518  imasival  13519  imasbas  13520  imasplusg  13521  imasmulr  13522  mgm1  13583  igsumvalx  13602  sgrp1  13624  mnd1  13668  mnd1id  13669  grp1  13819  grp1inv  13820  mulgnngsum  13844  triv1nsgd  13935  ring1  14203  znval  14784  znle  14785  znbaslemnn  14787  znbas  14792  znzrhval  14795  znzrhfo  14796  psrval  14814  psrbasg  14829  psrplusgg  14833  upgr1eopdc  16118  upgr1een  16119  umgr1een  16120  uspgr1eopdc  16238  usgr1eop  16240  1loopgrvd2fi  16300  1loopgrvd0fi  16301  p1evtxdeqfilem  16306  p1evtxdeqfi  16307  p1evtxdp1fi  16308  eupth2lem3fi  16471