Theorem pwexg 5372

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 4612	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2814	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5371	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3539	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  Vcvv 3470  𝒫 cpw 4598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5293  ax-pow 5359

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-in 3952  df-ss 3962  df-pw 4600

This theorem is referenced by:  pwexd  5373  pwex  5374  pwel  5375  abssexg  5376  snexALT  5377  xpexg  7746  uniexr  7759  pwexb  7762  fabexg  7936  pw2eng  9096  2pwne  9151  disjen  9152  domss2  9154  ssenen  9169  fineqvlem  9280  tskwe  9967  ween  10052  acni  10062  acnnum  10069  infpwfien  10079  pwdju1  10207  ackbij1b  10256  fictb  10262  fin2i  10312  isfin2-2  10336  ssfin3ds  10347  fin23lem32  10361  fin23lem39  10367  fin23lem41  10369  isfin1-3  10403  fin1a2lem12  10428  canth3  10578  ondomon  10580  canthnum  10666  canthwe  10668  gchxpidm  10686  hashbcval  16964  restid2  17405  prdsplusg  17433  prdsvsca  17435  ismre  17563  isacs1i  17630  sscpwex  17791  fpwipodrs  18525  acsdrscl  18531  opsrval  21977  toponsspwpw  22817  tgdom  22874  distop  22891  fctop  22900  cctop  22902  ppttop  22903  epttop  22905  cldval  22920  ntrfval  22921  clsfval  22922  neifval  22996  neif  22997  neival  22999  neiptoptop  23028  lpfval  23035  restfpw  23076  islocfin  23414  dissnref  23425  kgenval  23432  dfac14lem  23514  qtopval  23592  isfbas  23726  fbssfi  23734  fsubbas  23764  fgval  23767  filssufil  23809  hauspwpwf1  23884  hauspwpwdom  23885  flimfnfcls  23925  tsmsfbas  24025  eltsms  24030  ustval  24100  utopval  24130  madeval  27772  cusgrexilem1  29245  pwrssmgc  32721  indv  33625  sigaex  33723  sigaval  33724  pwsiga  33743  pwldsys  33770  ldgenpisyslem1  33776  omsval  33907  carsgval  33917  coinflipspace  34094  iscvm  34863  cvmsval  34870  ex-sategoelel  35025  altxpexg  35568  hfpw  35775  fnemeet2  35845  fnejoin1  35846  bj-restpw  36565  elrfi  42108  elrfirn  42109  kelac2  42483  enmappwid  43424  rfovd  43425  fsovrfovd  43433  dssmapfv2d  43442  clsk3nimkb  43464  clsneif1o  43528  clsneicnv  43529  clsneikex  43530  clsneinex  43531  neicvgmex  43541  neicvgel1  43543  pwsal  45697  prproropen  46842