Theorem pwexg 5315

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  𝒫 cpw 4542

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 5231  ax-pow 5302

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 3432  df-ss 3907  df-pw 4544

This theorem is referenced by:  pwexd  5316  pwex  5317  pwel  5318  abssexg  5319  snexALT  5320  xpexg  7697  uniexr  7710  pwexb  7713  fabexgOLD  7883  pw2eng  9014  2pwne  9064  disjen  9065  domss2  9067  ssenen  9082  fineqvlem  9169  tskwe  9865  ween  9948  acni  9958  acnnum  9965  infpwfien  9975  pwdju1  10104  ackbij1b  10151  fictb  10157  fin2i  10208  isfin2-2  10232  ssfin3ds  10243  fin23lem32  10257  fin23lem39  10263  fin23lem41  10265  isfin1-3  10299  fin1a2lem12  10324  canth3  10474  ondomon  10476  canthnum  10563  canthwe  10565  gchxpidm  10583  indv  12152  hashbcval  16964  restid2  17384  prdsplusg  17412  prdsvsca  17414  ismre  17543  isacs1i  17614  sscpwex  17773  fpwipodrs  18497  acsdrscl  18503  opsrval  22034  toponsspwpw  22897  tgdom  22953  distop  22970  fctop  22979  cctop  22981  ppttop  22982  epttop  22984  cldval  22998  ntrfval  22999  clsfval  23000  neifval  23074  neif  23075  neival  23077  neiptoptop  23106  lpfval  23113  restfpw  23154  islocfin  23492  dissnref  23503  kgenval  23510  dfac14lem  23592  qtopval  23670  isfbas  23804  fbssfi  23812  fsubbas  23842  fgval  23845  filssufil  23887  hauspwpwf1  23962  hauspwpwdom  23963  flimfnfcls  24003  tsmsfbas  24103  eltsms  24108  ustval  24178  utopval  24207  madeval  27838  cusgrexilem1  29522  pwrssmgc  33075  sigaex  34270  sigaval  34271  pwsiga  34290  pwldsys  34317  ldgenpisyslem1  34323  omsval  34453  carsgval  34463  coinflipspace  34641  iscvm  35457  cvmsval  35464  ex-sategoelel  35619  altxpexg  36176  hfpw  36383  fnemeet2  36565  fnejoin1  36566  bj-restpw  37420  elrfi  43140  elrfirn  43141  kelac2  43511  enmappwid  44445  rfovd  44446  fsovrfovd  44454  dssmapfv2d  44463  clsk3nimkb  44485  clsneif1o  44549  clsneicnv  44550  clsneikex  44551  clsneinex  44552  neicvgmex  44562  neicvgel1  44564  pwsal  46761  prproropen  47980  stgrvtx  48442  stgriedg  48443