Theorem pwexg 5344

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 4574	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2849	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5343	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3521	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Vcvv 3454  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pow 5331

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-pw 4562

This theorem is used by:  pwexd  5345  pwex  5346  pwel  5347  abssexg  5348  snexALT  5349  xpexg  7788  uniexr  7801  pwexb  7804  pw2eng  9130  2pwne  9180  disjen  9181  domss2  9183  ssenen  9198  fineqvlem  9285  hfpwOLD  9954  tskwe  10058  ween  10141  acni  10151  acnnum  10158  infpwfien  10168  pwdju1  10296  ackbij1b  10343  fictb  10349  fin2i  10400  isfin2-2  10424  ssfin3ds  10435  fin23lem32  10449  fin23lem39  10455  fin23lem41  10457  isfin1-3  10491  fin1a2lem12  10516  canth3  10672  ondomon  10674  canthnum  10761  canthwe  10763  gchxpidm  10781  indv  12349  hashbcval  17209  restid2  17630  prdsplusg  17658  prdsvsca  17660  ismre  17789  isacs1i  17860  sscpwex  18019  fpwipodrs  18743  acsdrscl  18749  opsrval  22385  toponsspwpw  23270  tgdom  23326  distop  23343  fctop  23352  cctop  23354  ppttop  23355  epttop  23357  cldval  23371  ntrfval  23372  clsfval  23373  neifval  23447  neif  23448  neival  23450  neiptoptop  23479  lpfval  23486  restfpw  23527  islocfin  23866  dissnref  23877  kgenval  23884  dfac14lem  23966  qtopval  24044  isfbas  24178  fbssfi  24186  fsubbas  24216  fgval  24219  filssufil  24261  hauspwpwf1  24336  hauspwpwdom  24337  flimfnfcls  24377  tsmsfbas  24477  eltsms  24482  ustval  24552  utopval  24581  madeval  28248  cusgrexilem1  30050  pwrssmgc  33631  reff  34541  sigaex  34812  sigaval  34813  pwsiga  34832  pwldsys  34860  ldgenpisyslem1  34866  omsval  34995  omssubadd  35002  carsgval  35005  coinflipspace  35183  iscvm  36191  cvmsval  36198  ex-sategoelel  36353  altxpexg  36921  fnemeet2  37333  fnejoin1  37334  bj-restpw  38204  elrfi  43898  elrfirn  43899  kelac2  44260  enmappwid  45192  rfovd  45193  fsovrfovd  45201  dssmapfv2d  45210  clsk3nimkb  45232  clsneif1o  45296  clsneicnv  45297  clsneikex  45298  clsneinex  45299  neicvgmex  45309  neicvgel1  45311  pwsal  47530  prproropen  48795  stgrvtx  49257  stgriedg  49258