Theorem pwexg 5353

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 4594	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2820	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5352	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3538	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3464  𝒫 cpw 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-pow 5340

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-pw 4582

This theorem is referenced by:  pwexd  5354  pwex  5355  pwel  5356  abssexg  5357  snexALT  5358  xpexg  7749  uniexr  7762  pwexb  7765  fabexgOLD  7940  pw2eng  9097  2pwne  9152  disjen  9153  domss2  9155  ssenen  9170  fineqvlem  9275  tskwe  9969  ween  10054  acni  10064  acnnum  10071  infpwfien  10081  pwdju1  10210  ackbij1b  10257  fictb  10263  fin2i  10314  isfin2-2  10338  ssfin3ds  10349  fin23lem32  10363  fin23lem39  10369  fin23lem41  10371  isfin1-3  10405  fin1a2lem12  10430  canth3  10580  ondomon  10582  canthnum  10668  canthwe  10670  gchxpidm  10688  hashbcval  17027  restid2  17449  prdsplusg  17477  prdsvsca  17479  ismre  17607  isacs1i  17674  sscpwex  17833  fpwipodrs  18555  acsdrscl  18561  opsrval  22009  toponsspwpw  22865  tgdom  22921  distop  22938  fctop  22947  cctop  22949  ppttop  22950  epttop  22952  cldval  22966  ntrfval  22967  clsfval  22968  neifval  23042  neif  23043  neival  23045  neiptoptop  23074  lpfval  23081  restfpw  23122  islocfin  23460  dissnref  23471  kgenval  23478  dfac14lem  23560  qtopval  23638  isfbas  23772  fbssfi  23780  fsubbas  23810  fgval  23813  filssufil  23855  hauspwpwf1  23930  hauspwpwdom  23931  flimfnfcls  23971  tsmsfbas  24071  eltsms  24076  ustval  24146  utopval  24176  madeval  27817  cusgrexilem1  29423  indv  32834  pwrssmgc  32985  sigaex  34146  sigaval  34147  pwsiga  34166  pwldsys  34193  ldgenpisyslem1  34199  omsval  34330  carsgval  34340  coinflipspace  34518  iscvm  35286  cvmsval  35293  ex-sategoelel  35448  altxpexg  36001  hfpw  36208  fnemeet2  36390  fnejoin1  36391  bj-restpw  37115  elrfi  42684  elrfirn  42685  kelac2  43056  enmappwid  43991  rfovd  43992  fsovrfovd  44000  dssmapfv2d  44009  clsk3nimkb  44031  clsneif1o  44095  clsneicnv  44096  clsneikex  44097  clsneinex  44098  neicvgmex  44108  neicvgel1  44110  pwsal  46311  prproropen  47489  stgrvtx  47933  stgriedg  47934