Theorem pwexg 5281

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 4557	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2899	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5280	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3569	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  Vcvv 3496  𝒫 cpw 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-pow 5268

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-pw 4543

This theorem is referenced by:  pwexd  5282  pwex  5283  pwel  5284  abssexg  5285  snexALT  5286  xpexg  7475  uniexr  7487  pwexb  7490  fabexg  7641  pw2eng  8625  2pwne  8675  disjen  8676  domss2  8678  ssenen  8693  fineqvlem  8734  tskwe  9381  ween  9463  acni  9473  acnnum  9480  infpwfien  9490  pwdju1  9618  ackbij1b  9663  fictb  9669  fin2i  9719  isfin2-2  9743  ssfin3ds  9754  fin23lem32  9768  fin23lem39  9774  fin23lem41  9776  isfin1-3  9810  fin1a2lem12  9835  canth3  9985  ondomon  9987  canthnum  10073  canthwe  10075  gchxpidm  10093  hashbcval  16340  restid2  16706  prdsplusg  16733  prdsvsca  16735  ismre  16863  isacs1i  16930  sscpwex  17087  fpwipodrs  17776  acsdrscl  17782  opsrval  20257  toponsspwpw  21532  tgdom  21588  distop  21605  fctop  21614  cctop  21616  ppttop  21617  epttop  21619  cldval  21633  ntrfval  21634  clsfval  21635  neifval  21709  neif  21710  neival  21712  neiptoptop  21741  lpfval  21748  restfpw  21789  islocfin  22127  dissnref  22138  kgenval  22145  dfac14lem  22227  qtopval  22305  isfbas  22439  fbssfi  22447  fsubbas  22477  fgval  22480  filssufil  22522  hauspwpwf1  22597  hauspwpwdom  22598  flimfnfcls  22638  tsmsfbas  22738  eltsms  22743  ustval  22813  utopval  22843  cusgrexilem1  27223  indv  31273  sigaex  31371  sigaval  31372  pwsiga  31391  pwldsys  31418  ldgenpisyslem1  31424  omsval  31553  carsgval  31563  coinflipspace  31740  iscvm  32508  cvmsval  32515  ex-sategoelel  32670  madeval  33291  altxpexg  33441  hfpw  33648  fnemeet2  33717  fnejoin1  33718  bj-restpw  34385  elrfi  39298  elrfirn  39299  kelac2  39672  enmappwid  40353  rfovd  40354  fsovrfovd  40362  dssmapfv2d  40371  clsk3nimkb  40397  clsneif1o  40461  clsneicnv  40462  clsneikex  40463  clsneinex  40464  neicvgmex  40474  neicvgel1  40476  pwsal  42607  prproropen  43677