Theorem pwexg 5314

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 4550	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2825	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5313	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3502	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3432  𝒫 cpw 4536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-pw 4538

This theorem is referenced by:  pwexd  5315  pwex  5316  pwel  5317  abssexg  5318  snexALT  5319  xpexg  7700  uniexr  7713  pwexb  7716  fabexgOLD  7886  pw2eng  9018  2pwne  9068  disjen  9069  domss2  9071  ssenen  9086  fineqvlem  9173  tskwe  9872  ween  9955  acni  9965  acnnum  9972  infpwfien  9982  pwdju1  10111  ackbij1b  10158  fictb  10164  fin2i  10215  isfin2-2  10239  ssfin3ds  10250  fin23lem32  10264  fin23lem39  10270  fin23lem41  10272  isfin1-3  10306  fin1a2lem12  10331  canth3  10481  ondomon  10483  canthnum  10570  canthwe  10572  gchxpidm  10590  indv  12159  hashbcval  16971  restid2  17391  prdsplusg  17419  prdsvsca  17421  ismre  17550  isacs1i  17621  sscpwex  17780  fpwipodrs  18504  acsdrscl  18510  opsrval  22029  toponsspwpw  22912  tgdom  22968  distop  22985  fctop  22994  cctop  22996  ppttop  22997  epttop  22999  cldval  23013  ntrfval  23014  clsfval  23015  neifval  23089  neif  23090  neival  23092  neiptoptop  23121  lpfval  23128  restfpw  23169  islocfin  23507  dissnref  23518  kgenval  23525  dfac14lem  23607  qtopval  23685  isfbas  23819  fbssfi  23827  fsubbas  23857  fgval  23860  filssufil  23902  hauspwpwf1  23977  hauspwpwdom  23978  flimfnfcls  24018  tsmsfbas  24118  eltsms  24123  ustval  24193  utopval  24222  madeval  27849  cusgrexilem1  29533  pwrssmgc  33086  sigaex  34301  sigaval  34302  pwsiga  34321  pwldsys  34348  ldgenpisyslem1  34354  omsval  34484  carsgval  34494  coinflipspace  34672  iscvm  35494  cvmsval  35501  ex-sategoelel  35656  altxpexg  36213  hfpw  36420  fnemeet2  36602  fnejoin1  36603  bj-restpw  37457  elrfi  43150  elrfirn  43151  kelac2  43517  enmappwid  44451  rfovd  44452  fsovrfovd  44460  dssmapfv2d  44469  clsk3nimkb  44491  clsneif1o  44555  clsneicnv  44556  clsneikex  44557  clsneinex  44558  neicvgmex  44568  neicvgel1  44570  pwsal  46765  prproropen  47990  stgrvtx  48452  stgriedg  48453