Theorem pwexg 5318

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 4563	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2818	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5317	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3508	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3437  𝒫 cpw 4549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-pow 5305

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-pw 4551

This theorem is referenced by:  pwexd  5319  pwex  5320  pwel  5321  abssexg  5322  snexALT  5323  xpexg  7689  uniexr  7702  pwexb  7705  fabexgOLD  7875  pw2eng  9003  2pwne  9053  disjen  9054  domss2  9056  ssenen  9071  fineqvlem  9157  tskwe  9850  ween  9933  acni  9943  acnnum  9950  infpwfien  9960  pwdju1  10089  ackbij1b  10136  fictb  10142  fin2i  10193  isfin2-2  10217  ssfin3ds  10228  fin23lem32  10242  fin23lem39  10248  fin23lem41  10250  isfin1-3  10284  fin1a2lem12  10309  canth3  10459  ondomon  10461  canthnum  10547  canthwe  10549  gchxpidm  10567  hashbcval  16916  restid2  17336  prdsplusg  17364  prdsvsca  17366  ismre  17494  isacs1i  17565  sscpwex  17724  fpwipodrs  18448  acsdrscl  18454  opsrval  21982  toponsspwpw  22838  tgdom  22894  distop  22911  fctop  22920  cctop  22922  ppttop  22923  epttop  22925  cldval  22939  ntrfval  22940  clsfval  22941  neifval  23015  neif  23016  neival  23018  neiptoptop  23047  lpfval  23054  restfpw  23095  islocfin  23433  dissnref  23444  kgenval  23451  dfac14lem  23533  qtopval  23611  isfbas  23745  fbssfi  23753  fsubbas  23783  fgval  23786  filssufil  23828  hauspwpwf1  23903  hauspwpwdom  23904  flimfnfcls  23944  tsmsfbas  24044  eltsms  24049  ustval  24119  utopval  24148  madeval  27794  cusgrexilem1  29419  indv  32838  pwrssmgc  32988  sigaex  34144  sigaval  34145  pwsiga  34164  pwldsys  34191  ldgenpisyslem1  34197  omsval  34327  carsgval  34337  coinflipspace  34515  iscvm  35324  cvmsval  35331  ex-sategoelel  35486  altxpexg  36043  hfpw  36250  fnemeet2  36432  fnejoin1  36433  bj-restpw  37157  elrfi  42812  elrfirn  42813  kelac2  43183  enmappwid  44118  rfovd  44119  fsovrfovd  44127  dssmapfv2d  44136  clsk3nimkb  44158  clsneif1o  44222  clsneicnv  44223  clsneikex  44224  clsneinex  44225  neicvgmex  44235  neicvgel1  44237  pwsal  46438  prproropen  47633  stgrvtx  48079  stgriedg  48080