Theorem pwexg 5340

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 4571	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2846	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5339	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3518	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3451  𝒫 cpw 4557

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-pw 4559

This theorem is used by:  pwexd  5341  pwex  5342  pwel  5343  abssexg  5344  snexALT  5345  xpexg  7753  uniexr  7766  pwexb  7769  pw2eng  9086  2pwne  9136  disjen  9137  domss2  9139  ssenen  9154  fineqvlem  9241  hfpwOLD  9908  tskwe  10012  ween  10095  acni  10105  acnnum  10112  infpwfien  10122  pwdju1  10250  ackbij1b  10297  fictb  10303  fin2i  10354  isfin2-2  10378  ssfin3ds  10389  fin23lem32  10403  fin23lem39  10409  fin23lem41  10411  isfin1-3  10445  fin1a2lem12  10470  canth3  10626  ondomon  10628  canthnum  10715  canthwe  10717  gchxpidm  10735  indv  12303  hashbcval  17160  restid2  17581  prdsplusg  17609  prdsvsca  17611  ismre  17740  isacs1i  17811  sscpwex  17970  fpwipodrs  18694  acsdrscl  18700  opsrval  22335  toponsspwpw  23220  tgdom  23276  distop  23293  fctop  23302  cctop  23304  ppttop  23305  epttop  23307  cldval  23321  ntrfval  23322  clsfval  23323  neifval  23397  neif  23398  neival  23400  neiptoptop  23429  lpfval  23436  restfpw  23477  islocfin  23816  dissnref  23827  kgenval  23834  dfac14lem  23916  qtopval  23994  isfbas  24128  fbssfi  24136  fsubbas  24166  fgval  24169  filssufil  24211  hauspwpwf1  24286  hauspwpwdom  24287  flimfnfcls  24327  tsmsfbas  24427  eltsms  24432  ustval  24502  utopval  24531  madeval  28200  cusgrexilem1  30002  pwrssmgc  33543  sigaex  34724  sigaval  34725  pwsiga  34744  pwldsys  34772  ldgenpisyslem1  34778  omsval  34908  carsgval  34918  coinflipspace  35096  iscvm  35993  cvmsval  36000  ex-sategoelel  36155  altxpexg  36713  fnemeet2  37125  fnejoin1  37126  bj-restpw  37981  elrfi  43658  elrfirn  43659  kelac2  44025  enmappwid  44959  rfovd  44960  fsovrfovd  44968  dssmapfv2d  44977  clsk3nimkb  44999  clsneif1o  45063  clsneicnv  45064  clsneikex  45065  clsneinex  45066  neicvgmex  45076  neicvgel1  45078  pwsal  47269  prproropen  48534  stgrvtx  48996  stgriedg  48997