Theorem pwexg 5347

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 2847	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5346	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3520	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3453  𝒫 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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pow 5334

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-pw 4562

This theorem is used by:  pwexd  5348  pwex  5349  pwel  5350  abssexg  5351  snexALT  5352  xpexg  7753  uniexr  7766  pwexb  7769  pw2eng  9085  2pwne  9135  disjen  9136  domss2  9138  ssenen  9153  fineqvlem  9240  tskwe  9959  ween  10042  acni  10052  acnnum  10059  infpwfien  10069  pwdju1  10197  ackbij1b  10244  fictb  10250  fin2i  10301  isfin2-2  10325  ssfin3ds  10336  fin23lem32  10350  fin23lem39  10356  fin23lem41  10358  isfin1-3  10392  fin1a2lem12  10417  canth3  10573  ondomon  10575  canthnum  10662  canthwe  10664  gchxpidm  10682  indv  12248  hashbcval  17100  restid2  17521  prdsplusg  17549  prdsvsca  17551  ismre  17680  isacs1i  17751  sscpwex  17910  fpwipodrs  18634  acsdrscl  18640  opsrval  22268  toponsspwpw  23153  tgdom  23209  distop  23226  fctop  23235  cctop  23237  ppttop  23238  epttop  23240  cldval  23254  ntrfval  23255  clsfval  23256  neifval  23330  neif  23331  neival  23333  neiptoptop  23362  lpfval  23369  restfpw  23410  islocfin  23749  dissnref  23760  kgenval  23767  dfac14lem  23849  qtopval  23927  isfbas  24061  fbssfi  24069  fsubbas  24099  fgval  24102  filssufil  24144  hauspwpwf1  24219  hauspwpwdom  24220  flimfnfcls  24260  tsmsfbas  24360  eltsms  24365  ustval  24435  utopval  24464  madeval  28105  cusgrexilem1  29907  pwrssmgc  33448  sigaex  34628  sigaval  34629  pwsiga  34648  pwldsys  34676  ldgenpisyslem1  34682  omsval  34812  carsgval  34822  coinflipspace  35000  iscvm  35846  cvmsval  35853  ex-sategoelel  36008  altxpexg  36566  hfpw  36773  fnemeet2  36994  fnejoin1  36995  bj-restpw  37850  elrfi  43547  elrfirn  43548  kelac2  43914  enmappwid  44848  rfovd  44849  fsovrfovd  44857  dssmapfv2d  44866  clsk3nimkb  44888  clsneif1o  44952  clsneicnv  44953  clsneikex  44954  clsneinex  44955  neicvgmex  44965  neicvgel1  44967  pwsal  47151  prproropen  48416  stgrvtx  48878  stgriedg  48879