Theorem pwexg 5358

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 4594	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2818	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5357	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3537	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  Vcvv 3463  𝒫 cpw 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-pow 5345

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-ss 3948  df-pw 4582

This theorem is referenced by:  pwexd  5359  pwex  5360  pwel  5361  abssexg  5362  snexALT  5363  xpexg  7752  uniexr  7765  pwexb  7768  fabexgOLD  7943  pw2eng  9100  2pwne  9155  disjen  9156  domss2  9158  ssenen  9173  fineqvlem  9280  tskwe  9972  ween  10057  acni  10067  acnnum  10074  infpwfien  10084  pwdju1  10213  ackbij1b  10260  fictb  10266  fin2i  10317  isfin2-2  10341  ssfin3ds  10352  fin23lem32  10366  fin23lem39  10372  fin23lem41  10374  isfin1-3  10408  fin1a2lem12  10433  canth3  10583  ondomon  10585  canthnum  10671  canthwe  10673  gchxpidm  10691  hashbcval  17022  restid2  17446  prdsplusg  17474  prdsvsca  17476  ismre  17604  isacs1i  17671  sscpwex  17830  fpwipodrs  18554  acsdrscl  18560  opsrval  22018  toponsspwpw  22876  tgdom  22932  distop  22949  fctop  22958  cctop  22960  ppttop  22961  epttop  22963  cldval  22977  ntrfval  22978  clsfval  22979  neifval  23053  neif  23054  neival  23056  neiptoptop  23085  lpfval  23092  restfpw  23133  islocfin  23471  dissnref  23482  kgenval  23489  dfac14lem  23571  qtopval  23649  isfbas  23783  fbssfi  23791  fsubbas  23821  fgval  23824  filssufil  23866  hauspwpwf1  23941  hauspwpwdom  23942  flimfnfcls  23982  tsmsfbas  24082  eltsms  24087  ustval  24157  utopval  24187  madeval  27827  cusgrexilem1  29384  indv  32777  pwrssmgc  32929  sigaex  34070  sigaval  34071  pwsiga  34090  pwldsys  34117  ldgenpisyslem1  34123  omsval  34254  carsgval  34264  coinflipspace  34442  iscvm  35223  cvmsval  35230  ex-sategoelel  35385  altxpexg  35938  hfpw  36145  fnemeet2  36327  fnejoin1  36328  bj-restpw  37052  elrfi  42668  elrfirn  42669  kelac2  43040  enmappwid  43975  rfovd  43976  fsovrfovd  43984  dssmapfv2d  43993  clsk3nimkb  44015  clsneif1o  44079  clsneicnv  44080  clsneikex  44081  clsneinex  44082  neicvgmex  44092  neicvgel1  44094  pwsal  46287  prproropen  47453  stgrvtx  47879  stgriedg  47880