Theorem pwexg 5351

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 4577	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2848	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5350	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3523	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  Vcvv 3455  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pow 5338

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-pw 4565

This theorem is referenced by:  pwexd  5352  pwex  5353  pwel  5354  abssexg  5355  snexALT  5356  xpexg  7750  uniexr  7763  pwexb  7766  pw2eng  9072  2pwne  9122  disjen  9123  domss2  9125  ssenen  9140  fineqvlem  9227  tskwe  9937  ween  10020  acni  10030  acnnum  10037  infpwfien  10047  pwdju1  10175  ackbij1b  10222  fictb  10228  fin2i  10280  isfin2-2  10304  ssfin3ds  10315  fin23lem32  10329  fin23lem39  10335  fin23lem41  10337  isfin1-3  10371  fin1a2lem12  10396  canth3  10546  ondomon  10548  canthnum  10635  canthwe  10637  gchxpidm  10655  indv  12221  hashbcval  17063  restid2  17484  prdsplusg  17512  prdsvsca  17514  ismre  17643  isacs1i  17714  sscpwex  17873  fpwipodrs  18597  acsdrscl  18603  opsrval  22178  toponsspwpw  23060  tgdom  23116  distop  23133  fctop  23142  cctop  23144  ppttop  23145  epttop  23147  cldval  23161  ntrfval  23162  clsfval  23163  neifval  23237  neif  23238  neival  23240  neiptoptop  23269  lpfval  23276  restfpw  23317  islocfin  23655  dissnref  23666  kgenval  23673  dfac14lem  23755  qtopval  23833  isfbas  23967  fbssfi  23975  fsubbas  24005  fgval  24008  filssufil  24050  hauspwpwf1  24125  hauspwpwdom  24126  flimfnfcls  24166  tsmsfbas  24266  eltsms  24271  ustval  24341  utopval  24370  madeval  28003  cusgrexilem1  29767  pwrssmgc  33298  sigaex  34478  sigaval  34479  pwsiga  34498  pwldsys  34525  ldgenpisyslem1  34531  omsval  34661  carsgval  34671  coinflipspace  34849  iscvm  35729  cvmsval  35736  ex-sategoelel  35891  altxpexg  36448  hfpw  36655  fnemeet2  36856  fnejoin1  36857  bj-restpw  37712  elrfi  43405  elrfirn  43406  kelac2  43772  enmappwid  44706  rfovd  44707  fsovrfovd  44715  dssmapfv2d  44724  clsk3nimkb  44746  clsneif1o  44810  clsneicnv  44811  clsneikex  44812  clsneinex  44813  neicvgmex  44823  neicvgel1  44825  pwsal  47009  prproropen  48234  stgrvtx  48696  stgriedg  48697