Theorem pwexg 5244

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 4513	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2874	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5243	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3515	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3441  𝒫 cpw 4497

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-pow 5231

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  pwexd  5245  pwex  5246  pwel  5247  abssexg  5248  snexALT  5249  xpexg  7453  uniexr  7465  pwexb  7468  fabexg  7621  pw2eng  8606  2pwne  8657  disjen  8658  domss2  8660  ssenen  8675  fineqvlem  8716  tskwe  9363  ween  9446  acni  9456  acnnum  9463  infpwfien  9473  pwdju1  9601  ackbij1b  9650  fictb  9656  fin2i  9706  isfin2-2  9730  ssfin3ds  9741  fin23lem32  9755  fin23lem39  9761  fin23lem41  9763  isfin1-3  9797  fin1a2lem12  9822  canth3  9972  ondomon  9974  canthnum  10060  canthwe  10062  gchxpidm  10080  hashbcval  16328  restid2  16696  prdsplusg  16723  prdsvsca  16725  ismre  16853  isacs1i  16920  sscpwex  17077  fpwipodrs  17766  acsdrscl  17772  opsrval  20714  toponsspwpw  21527  tgdom  21583  distop  21600  fctop  21609  cctop  21611  ppttop  21612  epttop  21614  cldval  21628  ntrfval  21629  clsfval  21630  neifval  21704  neif  21705  neival  21707  neiptoptop  21736  lpfval  21743  restfpw  21784  islocfin  22122  dissnref  22133  kgenval  22140  dfac14lem  22222  qtopval  22300  isfbas  22434  fbssfi  22442  fsubbas  22472  fgval  22475  filssufil  22517  hauspwpwf1  22592  hauspwpwdom  22593  flimfnfcls  22633  tsmsfbas  22733  eltsms  22738  ustval  22808  utopval  22838  cusgrexilem1  27229  pwrssmgc  30706  indv  31381  sigaex  31479  sigaval  31480  pwsiga  31499  pwldsys  31526  ldgenpisyslem1  31532  omsval  31661  carsgval  31671  coinflipspace  31848  iscvm  32619  cvmsval  32626  ex-sategoelel  32781  madeval  33402  altxpexg  33552  hfpw  33759  fnemeet2  33828  fnejoin1  33829  bj-restpw  34507  elrfi  39635  elrfirn  39636  kelac2  40009  enmappwid  40701  rfovd  40702  fsovrfovd  40710  dssmapfv2d  40719  clsk3nimkb  40743  clsneif1o  40807  clsneicnv  40808  clsneikex  40809  clsneinex  40810  neicvgmex  40820  neicvgel1  40822  pwsal  42957  prproropen  44025