Theorem pwexg 5375

Description: Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003.)

Assertion

Ref	Expression
pwexg	⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Proof of Theorem pwexg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pweq 4615	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2818	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5374	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3556	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474  𝒫 cpw 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-pow 5362

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-pw 4603

This theorem is referenced by:  pwexd  5376  pwex  5377  pwel  5378  abssexg  5379  snexALT  5380  xpexg  7733  uniexr  7746  pwexb  7749  fabexg  7921  pw2eng  9074  2pwne  9129  disjen  9130  domss2  9132  ssenen  9147  fineqvlem  9258  tskwe  9941  ween  10026  acni  10036  acnnum  10043  infpwfien  10053  pwdju1  10181  ackbij1b  10230  fictb  10236  fin2i  10286  isfin2-2  10310  ssfin3ds  10321  fin23lem32  10335  fin23lem39  10341  fin23lem41  10343  isfin1-3  10377  fin1a2lem12  10402  canth3  10552  ondomon  10554  canthnum  10640  canthwe  10642  gchxpidm  10660  hashbcval  16931  restid2  17372  prdsplusg  17400  prdsvsca  17402  ismre  17530  isacs1i  17597  sscpwex  17758  fpwipodrs  18489  acsdrscl  18495  opsrval  21592  toponsspwpw  22415  tgdom  22472  distop  22489  fctop  22498  cctop  22500  ppttop  22501  epttop  22503  cldval  22518  ntrfval  22519  clsfval  22520  neifval  22594  neif  22595  neival  22597  neiptoptop  22626  lpfval  22633  restfpw  22674  islocfin  23012  dissnref  23023  kgenval  23030  dfac14lem  23112  qtopval  23190  isfbas  23324  fbssfi  23332  fsubbas  23362  fgval  23365  filssufil  23407  hauspwpwf1  23482  hauspwpwdom  23483  flimfnfcls  23523  tsmsfbas  23623  eltsms  23628  ustval  23698  utopval  23728  madeval  27336  cusgrexilem1  28685  pwrssmgc  32157  indv  32998  sigaex  33096  sigaval  33097  pwsiga  33116  pwldsys  33143  ldgenpisyslem1  33149  omsval  33280  carsgval  33290  coinflipspace  33467  iscvm  34238  cvmsval  34245  ex-sategoelel  34400  altxpexg  34938  hfpw  35145  fnemeet2  35240  fnejoin1  35241  bj-restpw  35961  elrfi  41417  elrfirn  41418  kelac2  41792  enmappwid  42736  rfovd  42737  fsovrfovd  42745  dssmapfv2d  42754  clsk3nimkb  42776  clsneif1o  42840  clsneicnv  42841  clsneikex  42842  clsneinex  42843  neicvgmex  42853  neicvgel1  42855  pwsal  45017  prproropen  46162