Theorem pwexg 5132

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

Syntax hints:   → wi 4   = wceq 1507   ∈ wcel 2050  Vcvv 3415  𝒫 cpw 4422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-sep 5060  ax-pow 5119

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-v 3417  df-in 3836  df-ss 3843  df-pw 4424

This theorem is referenced by:  pwexd  5133  pwex  5134  abssexg  5135  snexALT  5136  pwel  5201  xpexg  7290  uniexr  7302  pwexb  7305  fabexg  7454  pw2eng  8419  2pwne  8469  disjen  8470  domss2  8472  ssenen  8487  fineqvlem  8527  tskwe  9173  ween  9255  acni  9265  acnnum  9272  infpwfien  9282  pwdju1  9414  ackbij1b  9459  fictb  9465  fin2i  9515  isfin2-2  9539  ssfin3ds  9550  fin23lem32  9564  fin23lem39  9570  fin23lem41  9572  isfin1-3  9606  fin1a2lem12  9631  canth3  9781  ondomon  9783  canthnum  9869  canthwe  9871  gchxpidm  9889  hashbcval  16194  restid2  16560  prdsplusg  16587  prdsvsca  16589  ismre  16719  isacs1i  16786  sscpwex  16943  fpwipodrs  17632  acsdrscl  17638  opsrval  19968  toponsspwpw  21234  tgdom  21290  distop  21307  fctop  21316  cctop  21318  ppttop  21319  epttop  21321  cldval  21335  ntrfval  21336  clsfval  21337  neifval  21411  neif  21412  neival  21414  neiptoptop  21443  lpfval  21450  restfpw  21491  islocfin  21829  dissnref  21840  kgenval  21847  dfac14lem  21929  qtopval  22007  isfbas  22141  fbssfi  22149  fsubbas  22179  fgval  22182  filssufil  22224  hauspwpwf1  22299  hauspwpwdom  22300  flimfnfcls  22340  tsmsfbas  22439  eltsms  22444  ustval  22514  utopval  22544  cusgrexilem1  26924  indv  30921  sigaex  31019  sigaval  31020  pwsiga  31040  pwldsys  31067  ldgenpisyslem1  31073  omsval  31202  carsgval  31212  coinflipspace  31390  iscvm  32097  cvmsval  32104  madeval  32816  altxpexg  32966  hfpw  33173  fnemeet2  33242  fnejoin1  33243  bj-restpw  33899  bj-discrmoore  33920  elrfi  38692  elrfirn  38693  kelac2  39067  enmappwid  39715  rfovd  39716  fsovrfovd  39724  dssmapfv2d  39733  clsk3nimkb  39759  clsneif1o  39823  clsneicnv  39824  clsneikex  39825  clsneinex  39826  neicvgmex  39836  neicvgel1  39838  pwsal  42037  prproropen  43044