Theorem pwexg 5396

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 4636	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2829	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5395	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3566	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  Vcvv 3488  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pow 5383

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-pw 4624

This theorem is referenced by:  pwexd  5397  pwex  5398  pwel  5399  abssexg  5400  snexALT  5401  xpexg  7785  uniexr  7798  pwexb  7801  fabexgOLD  7977  pw2eng  9144  2pwne  9199  disjen  9200  domss2  9202  ssenen  9217  fineqvlem  9325  tskwe  10019  ween  10104  acni  10114  acnnum  10121  infpwfien  10131  pwdju1  10260  ackbij1b  10307  fictb  10313  fin2i  10364  isfin2-2  10388  ssfin3ds  10399  fin23lem32  10413  fin23lem39  10419  fin23lem41  10421  isfin1-3  10455  fin1a2lem12  10480  canth3  10630  ondomon  10632  canthnum  10718  canthwe  10720  gchxpidm  10738  hashbcval  17049  restid2  17490  prdsplusg  17518  prdsvsca  17520  ismre  17648  isacs1i  17715  sscpwex  17876  fpwipodrs  18610  acsdrscl  18616  opsrval  22087  toponsspwpw  22949  tgdom  23006  distop  23023  fctop  23032  cctop  23034  ppttop  23035  epttop  23037  cldval  23052  ntrfval  23053  clsfval  23054  neifval  23128  neif  23129  neival  23131  neiptoptop  23160  lpfval  23167  restfpw  23208  islocfin  23546  dissnref  23557  kgenval  23564  dfac14lem  23646  qtopval  23724  isfbas  23858  fbssfi  23866  fsubbas  23896  fgval  23899  filssufil  23941  hauspwpwf1  24016  hauspwpwdom  24017  flimfnfcls  24057  tsmsfbas  24157  eltsms  24162  ustval  24232  utopval  24262  madeval  27909  cusgrexilem1  29474  pwrssmgc  32973  indv  33976  sigaex  34074  sigaval  34075  pwsiga  34094  pwldsys  34121  ldgenpisyslem1  34127  omsval  34258  carsgval  34268  coinflipspace  34445  iscvm  35227  cvmsval  35234  ex-sategoelel  35389  altxpexg  35942  hfpw  36149  fnemeet2  36333  fnejoin1  36334  bj-restpw  37058  elrfi  42650  elrfirn  42651  kelac2  43022  enmappwid  43962  rfovd  43963  fsovrfovd  43971  dssmapfv2d  43980  clsk3nimkb  44002  clsneif1o  44066  clsneicnv  44067  clsneikex  44068  clsneinex  44069  neicvgmex  44079  neicvgel1  44081  pwsal  46236  prproropen  47382