Theorem pwexg 5339

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 4570	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2845	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5338	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3517	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-pw 4558

This theorem is used by:  pwexd  5340  pwex  5341  pwel  5342  abssexg  5343  snexALT  5344  xpexg  7764  uniexr  7777  pwexb  7780  pw2eng  9105  2pwne  9155  disjen  9156  domss2  9158  ssenen  9173  fineqvlem  9260  hfpwOLD  9930  tskwe  10034  ween  10117  acni  10127  acnnum  10134  infpwfien  10144  pwdju1  10272  ackbij1b  10319  fictb  10325  fin2i  10376  isfin2-2  10400  ssfin3ds  10411  fin23lem32  10425  fin23lem39  10431  fin23lem41  10433  isfin1-3  10467  fin1a2lem12  10492  canth3  10648  ondomon  10650  canthnum  10737  canthwe  10739  gchxpidm  10757  indv  12325  hashbcval  17185  restid2  17606  prdsplusg  17634  prdsvsca  17636  ismre  17765  isacs1i  17836  sscpwex  17995  fpwipodrs  18719  acsdrscl  18725  opsrval  22360  toponsspwpw  23245  tgdom  23301  distop  23318  fctop  23327  cctop  23329  ppttop  23330  epttop  23332  cldval  23346  ntrfval  23347  clsfval  23348  neifval  23422  neif  23423  neival  23425  neiptoptop  23454  lpfval  23461  restfpw  23502  islocfin  23841  dissnref  23852  kgenval  23859  dfac14lem  23941  qtopval  24019  isfbas  24153  fbssfi  24161  fsubbas  24191  fgval  24194  filssufil  24236  hauspwpwf1  24311  hauspwpwdom  24312  flimfnfcls  24352  tsmsfbas  24452  eltsms  24457  ustval  24527  utopval  24556  madeval  28223  cusgrexilem1  30025  pwrssmgc  33607  reff  34517  sigaex  34788  sigaval  34789  pwsiga  34808  pwldsys  34836  ldgenpisyslem1  34842  omsval  34971  omssubadd  34978  carsgval  34981  coinflipspace  35159  iscvm  36110  cvmsval  36117  ex-sategoelel  36272  altxpexg  36835  fnemeet2  37247  fnejoin1  37248  bj-restpw  38105  elrfi  43798  elrfirn  43799  kelac2  44160  enmappwid  45093  rfovd  45094  fsovrfovd  45102  dssmapfv2d  45111  clsk3nimkb  45133  clsneif1o  45197  clsneicnv  45198  clsneikex  45199  clsneinex  45200  neicvgmex  45210  neicvgel1  45212  pwsal  47418  prproropen  48683  stgrvtx  49145  stgriedg  49146