Theorem pwexg 5377

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 4617	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2819	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5376	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3557	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-pow 5364

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  pwexd  5378  pwex  5379  pwel  5380  abssexg  5381  snexALT  5382  xpexg  7737  uniexr  7750  pwexb  7753  fabexg  7925  pw2eng  9078  2pwne  9133  disjen  9134  domss2  9136  ssenen  9151  fineqvlem  9262  tskwe  9945  ween  10030  acni  10040  acnnum  10047  infpwfien  10057  pwdju1  10185  ackbij1b  10234  fictb  10240  fin2i  10290  isfin2-2  10314  ssfin3ds  10325  fin23lem32  10339  fin23lem39  10345  fin23lem41  10347  isfin1-3  10381  fin1a2lem12  10406  canth3  10556  ondomon  10558  canthnum  10644  canthwe  10646  gchxpidm  10664  hashbcval  16935  restid2  17376  prdsplusg  17404  prdsvsca  17406  ismre  17534  isacs1i  17601  sscpwex  17762  fpwipodrs  18493  acsdrscl  18499  opsrval  21601  toponsspwpw  22424  tgdom  22481  distop  22498  fctop  22507  cctop  22509  ppttop  22510  epttop  22512  cldval  22527  ntrfval  22528  clsfval  22529  neifval  22603  neif  22604  neival  22606  neiptoptop  22635  lpfval  22642  restfpw  22683  islocfin  23021  dissnref  23032  kgenval  23039  dfac14lem  23121  qtopval  23199  isfbas  23333  fbssfi  23341  fsubbas  23371  fgval  23374  filssufil  23416  hauspwpwf1  23491  hauspwpwdom  23492  flimfnfcls  23532  tsmsfbas  23632  eltsms  23637  ustval  23707  utopval  23737  madeval  27347  cusgrexilem1  28696  pwrssmgc  32170  indv  33010  sigaex  33108  sigaval  33109  pwsiga  33128  pwldsys  33155  ldgenpisyslem1  33161  omsval  33292  carsgval  33302  coinflipspace  33479  iscvm  34250  cvmsval  34257  ex-sategoelel  34412  altxpexg  34950  hfpw  35157  fnemeet2  35252  fnejoin1  35253  bj-restpw  35973  elrfi  41432  elrfirn  41433  kelac2  41807  enmappwid  42751  rfovd  42752  fsovrfovd  42760  dssmapfv2d  42769  clsk3nimkb  42791  clsneif1o  42855  clsneicnv  42856  clsneikex  42857  clsneinex  42858  neicvgmex  42868  neicvgel1  42870  pwsal  45031  prproropen  46176