Theorem pwexg 5296

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 4546	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2823	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5295	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3495	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-pow 5283

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  pwexd  5297  pwex  5298  pwel  5299  abssexg  5300  snexALT  5301  xpexg  7578  uniexr  7591  pwexb  7594  fabexg  7755  pw2eng  8818  2pwne  8869  disjen  8870  domss2  8872  ssenen  8887  fineqvlem  8966  tskwe  9639  ween  9722  acni  9732  acnnum  9739  infpwfien  9749  pwdju1  9877  ackbij1b  9926  fictb  9932  fin2i  9982  isfin2-2  10006  ssfin3ds  10017  fin23lem32  10031  fin23lem39  10037  fin23lem41  10039  isfin1-3  10073  fin1a2lem12  10098  canth3  10248  ondomon  10250  canthnum  10336  canthwe  10338  gchxpidm  10356  hashbcval  16631  restid2  17058  prdsplusg  17086  prdsvsca  17088  ismre  17216  isacs1i  17283  sscpwex  17444  fpwipodrs  18173  acsdrscl  18179  opsrval  21157  toponsspwpw  21979  tgdom  22036  distop  22053  fctop  22062  cctop  22064  ppttop  22065  epttop  22067  cldval  22082  ntrfval  22083  clsfval  22084  neifval  22158  neif  22159  neival  22161  neiptoptop  22190  lpfval  22197  restfpw  22238  islocfin  22576  dissnref  22587  kgenval  22594  dfac14lem  22676  qtopval  22754  isfbas  22888  fbssfi  22896  fsubbas  22926  fgval  22929  filssufil  22971  hauspwpwf1  23046  hauspwpwdom  23047  flimfnfcls  23087  tsmsfbas  23187  eltsms  23192  ustval  23262  utopval  23292  cusgrexilem1  27709  pwrssmgc  31180  indv  31880  sigaex  31978  sigaval  31979  pwsiga  31998  pwldsys  32025  ldgenpisyslem1  32031  omsval  32160  carsgval  32170  coinflipspace  32347  iscvm  33121  cvmsval  33128  ex-sategoelel  33283  madeval  33963  altxpexg  34207  hfpw  34414  fnemeet2  34483  fnejoin1  34484  bj-restpw  35190  elrfi  40432  elrfirn  40433  kelac2  40806  enmappwid  41497  rfovd  41498  fsovrfovd  41506  dssmapfv2d  41515  clsk3nimkb  41539  clsneif1o  41603  clsneicnv  41604  clsneikex  41605  clsneinex  41606  neicvgmex  41616  neicvgel1  41618  pwsal  43746  prproropen  44848