Theorem pwexg 5340

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 4572	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2850	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5339	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3525	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  Vcvv 3457  𝒫 cpw 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pow 5327

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-pw 4560

This theorem is referenced by:  pwexd  5341  pwex  5342  pwel  5343  abssexg  5344  snexALT  5345  xpexg  7737  uniexr  7750  pwexb  7753  pw2eng  9059  2pwne  9109  disjen  9110  domss2  9112  ssenen  9127  fineqvlem  9214  tskwe  9924  ween  10007  acni  10017  acnnum  10024  infpwfien  10034  pwdju1  10162  ackbij1b  10209  fictb  10215  fin2i  10267  isfin2-2  10291  ssfin3ds  10302  fin23lem32  10316  fin23lem39  10322  fin23lem41  10324  isfin1-3  10358  fin1a2lem12  10383  canth3  10533  ondomon  10535  canthnum  10622  canthwe  10624  gchxpidm  10642  indv  12211  hashbcval  17052  restid2  17473  prdsplusg  17501  prdsvsca  17503  ismre  17632  isacs1i  17703  sscpwex  17862  fpwipodrs  18586  acsdrscl  18592  opsrval  22157  toponsspwpw  23040  tgdom  23096  distop  23113  fctop  23122  cctop  23124  ppttop  23125  epttop  23127  cldval  23141  ntrfval  23142  clsfval  23143  neifval  23217  neif  23218  neival  23220  neiptoptop  23249  lpfval  23256  restfpw  23297  islocfin  23635  dissnref  23646  kgenval  23653  dfac14lem  23735  qtopval  23813  isfbas  23947  fbssfi  23955  fsubbas  23985  fgval  23988  filssufil  24030  hauspwpwf1  24105  hauspwpwdom  24106  flimfnfcls  24146  tsmsfbas  24246  eltsms  24251  ustval  24321  utopval  24350  madeval  27983  cusgrexilem1  29698  pwrssmgc  33233  sigaex  34417  sigaval  34418  pwsiga  34437  pwldsys  34464  ldgenpisyslem1  34470  omsval  34600  carsgval  34610  coinflipspace  34788  iscvm  35622  cvmsval  35629  ex-sategoelel  35784  altxpexg  36341  hfpw  36548  fnemeet2  36740  fnejoin1  36741  bj-restpw  37594  elrfi  43287  elrfirn  43288  kelac2  43654  enmappwid  44588  rfovd  44589  fsovrfovd  44597  dssmapfv2d  44606  clsk3nimkb  44628  clsneif1o  44692  clsneicnv  44693  clsneikex  44694  clsneinex  44695  neicvgmex  44705  neicvgel1  44707  pwsal  46887  prproropen  48112  stgrvtx  48574  stgriedg  48575