Theorem pwexg 5320

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 4555	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2821	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5319	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3499	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3429  𝒫 cpw 4541

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 2708  ax-sep 5231  ax-pow 5307

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-pw 4543

This theorem is referenced by:  pwexd  5321  pwex  5322  pwel  5323  abssexg  5324  snexALT  5325  xpexg  7704  uniexr  7717  pwexb  7720  fabexgOLD  7890  pw2eng  9021  2pwne  9071  disjen  9072  domss2  9074  ssenen  9089  fineqvlem  9176  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  indv  12161  hashbcval  16973  restid2  17393  prdsplusg  17421  prdsvsca  17423  ismre  17552  isacs1i  17623  sscpwex  17782  fpwipodrs  18506  acsdrscl  18512  opsrval  22024  toponsspwpw  22887  tgdom  22943  distop  22960  fctop  22969  cctop  22971  ppttop  22972  epttop  22974  cldval  22988  ntrfval  22989  clsfval  22990  neifval  23064  neif  23065  neival  23067  neiptoptop  23096  lpfval  23103  restfpw  23144  islocfin  23482  dissnref  23493  kgenval  23500  dfac14lem  23582  qtopval  23660  isfbas  23794  fbssfi  23802  fsubbas  23832  fgval  23835  filssufil  23877  hauspwpwf1  23952  hauspwpwdom  23953  flimfnfcls  23993  tsmsfbas  24093  eltsms  24098  ustval  24168  utopval  24197  madeval  27824  cusgrexilem1  29508  pwrssmgc  33060  sigaex  34254  sigaval  34255  pwsiga  34274  pwldsys  34301  ldgenpisyslem1  34307  omsval  34437  carsgval  34447  coinflipspace  34625  iscvm  35441  cvmsval  35448  ex-sategoelel  35603  altxpexg  36160  hfpw  36367  fnemeet2  36549  fnejoin1  36550  bj-restpw  37404  elrfi  43126  elrfirn  43127  kelac2  43493  enmappwid  44427  rfovd  44428  fsovrfovd  44436  dssmapfv2d  44445  clsk3nimkb  44467  clsneif1o  44531  clsneicnv  44532  clsneikex  44533  clsneinex  44534  neicvgmex  44544  neicvgel1  44546  pwsal  46743  prproropen  47968  stgrvtx  48430  stgriedg  48431