Theorem pwexg 5320

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 4567	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2813	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5319	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3511	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3438  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-pow 5307

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-pw 4555

This theorem is referenced by:  pwexd  5321  pwex  5322  pwel  5323  abssexg  5324  snexALT  5325  xpexg  7690  uniexr  7703  pwexb  7706  fabexgOLD  7879  pw2eng  9007  2pwne  9057  disjen  9058  domss2  9060  ssenen  9075  fineqvlem  9167  tskwe  9865  ween  9948  acni  9958  acnnum  9965  infpwfien  9975  pwdju1  10104  ackbij1b  10151  fictb  10157  fin2i  10208  isfin2-2  10232  ssfin3ds  10243  fin23lem32  10257  fin23lem39  10263  fin23lem41  10265  isfin1-3  10299  fin1a2lem12  10324  canth3  10474  ondomon  10476  canthnum  10562  canthwe  10564  gchxpidm  10582  hashbcval  16932  restid2  17352  prdsplusg  17380  prdsvsca  17382  ismre  17510  isacs1i  17581  sscpwex  17740  fpwipodrs  18464  acsdrscl  18470  opsrval  21969  toponsspwpw  22825  tgdom  22881  distop  22898  fctop  22907  cctop  22909  ppttop  22910  epttop  22912  cldval  22926  ntrfval  22927  clsfval  22928  neifval  23002  neif  23003  neival  23005  neiptoptop  23034  lpfval  23041  restfpw  23082  islocfin  23420  dissnref  23431  kgenval  23438  dfac14lem  23520  qtopval  23598  isfbas  23732  fbssfi  23740  fsubbas  23770  fgval  23773  filssufil  23815  hauspwpwf1  23890  hauspwpwdom  23891  flimfnfcls  23931  tsmsfbas  24031  eltsms  24036  ustval  24106  utopval  24136  madeval  27780  cusgrexilem1  29402  indv  32808  pwrssmgc  32955  sigaex  34079  sigaval  34080  pwsiga  34099  pwldsys  34126  ldgenpisyslem1  34132  omsval  34263  carsgval  34273  coinflipspace  34451  iscvm  35234  cvmsval  35241  ex-sategoelel  35396  altxpexg  35954  hfpw  36161  fnemeet2  36343  fnejoin1  36344  bj-restpw  37068  elrfi  42670  elrfirn  42671  kelac2  43041  enmappwid  43976  rfovd  43977  fsovrfovd  43985  dssmapfv2d  43994  clsk3nimkb  44016  clsneif1o  44080  clsneicnv  44081  clsneikex  44082  clsneinex  44083  neicvgmex  44093  neicvgel1  44095  pwsal  46300  prproropen  47496  stgrvtx  47942  stgriedg  47943