Theorem pweqd 4546

Description: Equality deduction for power class. (Contributed by NM, 27-Nov-2013.)

Hypothesis

Ref	Expression
pweqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
pweqd	⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)

Proof of Theorem pweqd

Step	Hyp	Ref	Expression
1		pweqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		pweq 4543	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1547  𝒫 cpw 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-pw 4531

This theorem is referenced by:  undefval  8216  pmvalg  8774  marypha1lem  9336  marypha1  9337  r1val3  9753  ackbij2lem2  10152  ackbij2lem3  10153  r1om  10156  isfin2  10207  hsmexlem8  10337  vdwmc  16940  hashbcval  16964  ismre  17543  mrcfval  17565  mrisval  17587  mreexexlemd  17601  brssc  17772  lubfval  18305  glbfval  18318  isclat  18457  issubmgm  18661  issubm  18762  issubg  19093  cntzfval  19286  lsmfval  19604  lsmpropd  19643  pj1fval  19660  issubrng  20519  issubrg  20543  rgspnval  20584  lssset  20923  lspfval  20963  lsppropd  21008  islbs  21066  sraval  21165  ocvfval  21641  isobs  21695  islinds  21784  aspval  21847  opsrval  22022  ply1frcl  22304  evls1fval  22305  basis1  22933  baspartn  22937  cldval  23006  ntrfval  23007  clsfval  23008  mretopd  23075  neifval  23082  lpfval  23121  cncls2  23256  iscnrm  23306  iscnrm2  23321  2ndcsep  23442  kgenval  23518  xkoval  23570  dfac14  23601  qtopval  23678  qtopval2  23679  isfbas  23812  trfbas2  23826  flimval  23946  elflim  23954  flimclslem  23967  fclsfnflim  24010  fclscmp  24013  tsmsfbas  24111  tsmsval2  24113  ustval  24186  utopval  24215  mopnfss  24426  setsmstopn  24461  met2ndc  24506  madeval  27842  elmade2  27868  istrkgb  28541  isuhgr  29147  isushgr  29148  isuhgrop  29157  uhgrun  29161  uhgrstrrepe  29165  isupgr  29171  upgrop  29181  isumgr  29182  upgrun  29205  umgrun  29207  isuspgr  29239  isusgr  29240  isuspgrop  29248  isusgrop  29249  ausgrusgrb  29252  usgrstrrepe  29322  issubgr  29358  uhgrspansubgrlem  29377  usgrexi  29528  1hevtxdg1  29593  umgr2v2e  29612  zarcmplem  34065  ismeas  34383  omsval  34477  omscl  34479  omsf  34480  oms0  34481  carsgval  34487  omsmeas  34507  erdszelem3  35421  erdsze  35430  kur14  35444  iscvm  35487  mpstval  35763  mclsval  35791  mh-infprim2bi  36775  bj-imdirvallem  37540  pibp21  37777  heibor  38188  idlval  38380  igenval  38428  paddfval  40289  pclfvalN  40381  polfvalN  40396  docaffvalN  41613  docafvalN  41614  djaffvalN  41625  djafvalN  41626  dochffval  41841  dochfval  41842  djhffval  41888  djhfval  41889  lpolsetN  41974  lcdlss2N  42112  mzpclval  43174  dfac21  43511  islmodfg  43514  islssfg  43515  rfovd  44445  fsovrfovd  44453  gneispace2  44576  ismnu  44705  sge0val  46809  ismea  46894  psmeasure  46914  caragenval  46936  isome  46937  omeunile  46948  isomennd  46974  ovnval  46984  hspmbl  47072  isvonmbl  47081  afv2eq12d  47678  isisubgr  48353  isubgruhgr  48359  stgrfv  48444  stgrusgra  48450  gpgov  48533  gpgusgra  48548  lincop  48899  lcoop  48902  islininds  48937  ldepsnlinc  48999  isclatd  49473