Theorem pwexg 5325

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 4570	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2822	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5324	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3513	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-pw 4558

This theorem is referenced by:  pwexd  5326  pwex  5327  pwel  5328  abssexg  5329  snexALT  5330  xpexg  7705  uniexr  7718  pwexb  7721  fabexgOLD  7891  pw2eng  9023  2pwne  9073  disjen  9074  domss2  9076  ssenen  9091  fineqvlem  9178  tskwe  9874  ween  9957  acni  9967  acnnum  9974  infpwfien  9984  pwdju1  10113  ackbij1b  10160  fictb  10166  fin2i  10217  isfin2-2  10241  ssfin3ds  10252  fin23lem32  10266  fin23lem39  10272  fin23lem41  10274  isfin1-3  10308  fin1a2lem12  10333  canth3  10483  ondomon  10485  canthnum  10572  canthwe  10574  gchxpidm  10592  hashbcval  16942  restid2  17362  prdsplusg  17390  prdsvsca  17392  ismre  17521  isacs1i  17592  sscpwex  17751  fpwipodrs  18475  acsdrscl  18481  opsrval  22013  toponsspwpw  22878  tgdom  22934  distop  22951  fctop  22960  cctop  22962  ppttop  22963  epttop  22965  cldval  22979  ntrfval  22980  clsfval  22981  neifval  23055  neif  23056  neival  23058  neiptoptop  23087  lpfval  23094  restfpw  23135  islocfin  23473  dissnref  23484  kgenval  23491  dfac14lem  23573  qtopval  23651  isfbas  23785  fbssfi  23793  fsubbas  23823  fgval  23826  filssufil  23868  hauspwpwf1  23943  hauspwpwdom  23944  flimfnfcls  23984  tsmsfbas  24084  eltsms  24089  ustval  24159  utopval  24188  madeval  27840  cusgrexilem1  29524  indv  32941  pwrssmgc  33092  sigaex  34287  sigaval  34288  pwsiga  34307  pwldsys  34334  ldgenpisyslem1  34340  omsval  34470  carsgval  34480  coinflipspace  34658  iscvm  35472  cvmsval  35479  ex-sategoelel  35634  altxpexg  36191  hfpw  36398  fnemeet2  36580  fnejoin1  36581  bj-restpw  37342  elrfi  43048  elrfirn  43049  kelac2  43419  enmappwid  44353  rfovd  44354  fsovrfovd  44362  dssmapfv2d  44371  clsk3nimkb  44393  clsneif1o  44457  clsneicnv  44458  clsneikex  44459  clsneinex  44460  neicvgmex  44470  neicvgel1  44472  pwsal  46670  prproropen  47865  stgrvtx  48311  stgriedg  48312