Theorem pwexg 5333

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 4577	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2813	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5332	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3520	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-pow 5320

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-pw 4565

This theorem is referenced by:  pwexd  5334  pwex  5335  pwel  5336  abssexg  5337  snexALT  5338  xpexg  7726  uniexr  7739  pwexb  7742  fabexgOLD  7915  pw2eng  9047  2pwne  9097  disjen  9098  domss2  9100  ssenen  9115  fineqvlem  9209  tskwe  9903  ween  9988  acni  9998  acnnum  10005  infpwfien  10015  pwdju1  10144  ackbij1b  10191  fictb  10197  fin2i  10248  isfin2-2  10272  ssfin3ds  10283  fin23lem32  10297  fin23lem39  10303  fin23lem41  10305  isfin1-3  10339  fin1a2lem12  10364  canth3  10514  ondomon  10516  canthnum  10602  canthwe  10604  gchxpidm  10622  hashbcval  16973  restid2  17393  prdsplusg  17421  prdsvsca  17423  ismre  17551  isacs1i  17618  sscpwex  17777  fpwipodrs  18499  acsdrscl  18505  opsrval  21953  toponsspwpw  22809  tgdom  22865  distop  22882  fctop  22891  cctop  22893  ppttop  22894  epttop  22896  cldval  22910  ntrfval  22911  clsfval  22912  neifval  22986  neif  22987  neival  22989  neiptoptop  23018  lpfval  23025  restfpw  23066  islocfin  23404  dissnref  23415  kgenval  23422  dfac14lem  23504  qtopval  23582  isfbas  23716  fbssfi  23724  fsubbas  23754  fgval  23757  filssufil  23799  hauspwpwf1  23874  hauspwpwdom  23875  flimfnfcls  23915  tsmsfbas  24015  eltsms  24020  ustval  24090  utopval  24120  madeval  27760  cusgrexilem1  29366  indv  32775  pwrssmgc  32926  sigaex  34100  sigaval  34101  pwsiga  34120  pwldsys  34147  ldgenpisyslem1  34153  omsval  34284  carsgval  34294  coinflipspace  34472  iscvm  35246  cvmsval  35253  ex-sategoelel  35408  altxpexg  35966  hfpw  36173  fnemeet2  36355  fnejoin1  36356  bj-restpw  37080  elrfi  42682  elrfirn  42683  kelac2  43054  enmappwid  43989  rfovd  43990  fsovrfovd  43998  dssmapfv2d  44007  clsk3nimkb  44029  clsneif1o  44093  clsneicnv  44094  clsneikex  44095  clsneinex  44096  neicvgmex  44106  neicvgel1  44108  pwsal  46313  prproropen  47506  stgrvtx  47950  stgriedg  47951