Theorem pwexg 5354

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 4581	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2851	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5353	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3525	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  Vcvv 3458  𝒫 cpw 4567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pow 5341

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-pw 4569

This theorem is used by:  pwexd  5355  pwex  5356  pwel  5357  abssexg  5358  snexALT  5359  xpexg  7758  uniexr  7771  pwexb  7774  pw2eng  9081  2pwne  9131  disjen  9132  domss2  9134  ssenen  9149  fineqvlem  9236  tskwe  9955  ween  10038  acni  10048  acnnum  10055  infpwfien  10065  pwdju1  10193  ackbij1b  10240  fictb  10246  fin2i  10297  isfin2-2  10321  ssfin3ds  10332  fin23lem32  10346  fin23lem39  10352  fin23lem41  10354  isfin1-3  10388  fin1a2lem12  10413  canth3  10563  ondomon  10565  canthnum  10652  canthwe  10654  gchxpidm  10672  indv  12238  hashbcval  17087  restid2  17508  prdsplusg  17536  prdsvsca  17538  ismre  17667  isacs1i  17738  sscpwex  17897  fpwipodrs  18621  acsdrscl  18627  opsrval  22234  toponsspwpw  23116  tgdom  23172  distop  23189  fctop  23198  cctop  23200  ppttop  23201  epttop  23203  cldval  23217  ntrfval  23218  clsfval  23219  neifval  23293  neif  23294  neival  23296  neiptoptop  23325  lpfval  23332  restfpw  23373  islocfin  23711  dissnref  23722  kgenval  23729  dfac14lem  23811  qtopval  23889  isfbas  24023  fbssfi  24031  fsubbas  24061  fgval  24064  filssufil  24106  hauspwpwf1  24181  hauspwpwdom  24182  flimfnfcls  24222  tsmsfbas  24322  eltsms  24327  ustval  24397  utopval  24426  madeval  28062  cusgrexilem1  29826  pwrssmgc  33351  sigaex  34531  sigaval  34532  pwsiga  34551  pwldsys  34579  ldgenpisyslem1  34585  omsval  34715  carsgval  34725  coinflipspace  34903  iscvm  35772  cvmsval  35779  ex-sategoelel  35934  altxpexg  36491  hfpw  36698  fnemeet2  36919  fnejoin1  36920  bj-restpw  37775  elrfi  43466  elrfirn  43467  kelac2  43833  enmappwid  44767  rfovd  44768  fsovrfovd  44776  dssmapfv2d  44785  clsk3nimkb  44807  clsneif1o  44871  clsneicnv  44872  clsneikex  44873  clsneinex  44874  neicvgmex  44884  neicvgel1  44886  pwsal  47070  prproropen  48298  stgrvtx  48760  stgriedg  48761