Theorem pwexg 5313

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 4556	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2822	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5312	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3500	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pow 5300

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-pw 4544

This theorem is referenced by:  pwexd  5314  pwex  5315  pwel  5316  abssexg  5317  snexALT  5318  xpexg  7695  uniexr  7708  pwexb  7711  fabexgOLD  7881  pw2eng  9012  2pwne  9062  disjen  9063  domss2  9065  ssenen  9080  fineqvlem  9167  tskwe  9863  ween  9946  acni  9956  acnnum  9963  infpwfien  9973  pwdju1  10102  ackbij1b  10149  fictb  10155  fin2i  10206  isfin2-2  10230  ssfin3ds  10241  fin23lem32  10255  fin23lem39  10261  fin23lem41  10263  isfin1-3  10297  fin1a2lem12  10322  canth3  10472  ondomon  10474  canthnum  10561  canthwe  10563  gchxpidm  10581  indv  12150  hashbcval  16962  restid2  17382  prdsplusg  17410  prdsvsca  17412  ismre  17541  isacs1i  17612  sscpwex  17771  fpwipodrs  18495  acsdrscl  18501  opsrval  22033  toponsspwpw  22896  tgdom  22952  distop  22969  fctop  22978  cctop  22980  ppttop  22981  epttop  22983  cldval  22997  ntrfval  22998  clsfval  22999  neifval  23073  neif  23074  neival  23076  neiptoptop  23105  lpfval  23112  restfpw  23153  islocfin  23491  dissnref  23502  kgenval  23509  dfac14lem  23591  qtopval  23669  isfbas  23803  fbssfi  23811  fsubbas  23841  fgval  23844  filssufil  23886  hauspwpwf1  23961  hauspwpwdom  23962  flimfnfcls  24002  tsmsfbas  24102  eltsms  24107  ustval  24177  utopval  24206  madeval  27843  cusgrexilem1  29527  pwrssmgc  33080  sigaex  34275  sigaval  34276  pwsiga  34295  pwldsys  34322  ldgenpisyslem1  34328  omsval  34458  carsgval  34468  coinflipspace  34646  iscvm  35462  cvmsval  35469  ex-sategoelel  35624  altxpexg  36181  hfpw  36388  fnemeet2  36570  fnejoin1  36571  bj-restpw  37417  elrfi  43137  elrfirn  43138  kelac2  43508  enmappwid  44442  rfovd  44443  fsovrfovd  44451  dssmapfv2d  44460  clsk3nimkb  44482  clsneif1o  44546  clsneicnv  44547  clsneikex  44548  clsneinex  44549  neicvgmex  44559  neicvgel1  44561  pwsal  46758  prproropen  47965  stgrvtx  48427  stgriedg  48428