Theorem pwexg 5302

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 4550	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2824	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5301	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3506	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  Vcvv 3433  𝒫 cpw 4534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-pow 5289

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-pw 4536

This theorem is referenced by:  pwexd  5303  pwex  5304  pwel  5305  abssexg  5306  snexALT  5307  xpexg  7609  uniexr  7622  pwexb  7625  fabexg  7790  pw2eng  8874  2pwne  8929  disjen  8930  domss2  8932  ssenen  8947  fineqvlem  9046  tskwe  9717  ween  9800  acni  9810  acnnum  9817  infpwfien  9827  pwdju1  9955  ackbij1b  10004  fictb  10010  fin2i  10060  isfin2-2  10084  ssfin3ds  10095  fin23lem32  10109  fin23lem39  10115  fin23lem41  10117  isfin1-3  10151  fin1a2lem12  10176  canth3  10326  ondomon  10328  canthnum  10414  canthwe  10416  gchxpidm  10434  hashbcval  16712  restid2  17150  prdsplusg  17178  prdsvsca  17180  ismre  17308  isacs1i  17375  sscpwex  17536  fpwipodrs  18267  acsdrscl  18273  opsrval  21256  toponsspwpw  22080  tgdom  22137  distop  22154  fctop  22163  cctop  22165  ppttop  22166  epttop  22168  cldval  22183  ntrfval  22184  clsfval  22185  neifval  22259  neif  22260  neival  22262  neiptoptop  22291  lpfval  22298  restfpw  22339  islocfin  22677  dissnref  22688  kgenval  22695  dfac14lem  22777  qtopval  22855  isfbas  22989  fbssfi  22997  fsubbas  23027  fgval  23030  filssufil  23072  hauspwpwf1  23147  hauspwpwdom  23148  flimfnfcls  23188  tsmsfbas  23288  eltsms  23293  ustval  23363  utopval  23393  cusgrexilem1  27815  pwrssmgc  31287  indv  31989  sigaex  32087  sigaval  32088  pwsiga  32107  pwldsys  32134  ldgenpisyslem1  32140  omsval  32269  carsgval  32279  coinflipspace  32456  iscvm  33230  cvmsval  33237  ex-sategoelel  33392  madeval  34045  altxpexg  34289  hfpw  34496  fnemeet2  34565  fnejoin1  34566  bj-restpw  35272  elrfi  40523  elrfirn  40524  kelac2  40897  enmappwid  41615  rfovd  41616  fsovrfovd  41624  dssmapfv2d  41633  clsk3nimkb  41657  clsneif1o  41721  clsneicnv  41722  clsneikex  41723  clsneinex  41724  neicvgmex  41734  neicvgel1  41736  pwsal  43863  prproropen  44971