Theorem pweqd 4579

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 4576	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1570  𝒫 cpw 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-pw 4564

This theorem is referenced by:  undefval  8269  pmvalg  8830  marypha1lem  9389  marypha1  9390  r1val3  9806  ackbij2lem2  10218  ackbij2lem3  10219  r1om  10222  isfin2  10273  hsmexlem8  10403  vdwmc  17033  hashbcval  17057  ismre  17637  mrcfval  17659  mrisval  17681  mreexexlemd  17695  brssc  17866  lubfval  18399  glbfval  18412  isclat  18551  issubmgm  18755  issubm  18856  issubg  19187  cntzfval  19385  lsmfval  19703  lsmpropd  19742  pj1fval  19759  issubrng  20646  issubrg  20670  rgspnval  20711  lssset  21054  lspfval  21094  lsppropd  21139  islbs  21197  sraval  21296  ocvfval  21816  isobs  21870  islinds  21959  aspval  22022  opsrval  22197  ply1frcl  22478  evls1fval  22479  basis1  23107  baspartn  23111  cldval  23180  ntrfval  23181  clsfval  23182  mretopd  23249  neifval  23256  lpfval  23295  cncls2  23430  iscnrm  23480  iscnrm2  23495  2ndcsep  23616  kgenval  23692  xkoval  23744  dfac14  23775  qtopval  23852  qtopval2  23853  isfbas  23986  trfbas2  24000  flimval  24120  elflim  24128  flimclslem  24141  fclsfnflim  24184  fclscmp  24187  tsmsfbas  24285  tsmsval2  24287  ustval  24360  utopval  24389  mopnfss  24600  setsmstopn  24635  met2ndc  24680  madeval  28025  elmade2  28051  istrkgb  28724  isuhgr  29410  isushgr  29411  isuhgrop  29420  uhgrun  29424  uhgrstrrepe  29428  isupgr  29434  upgrop  29444  isumgr  29445  upgrun  29468  umgrun  29470  isuspgr  29502  isusgr  29503  isuspgrop  29511  isusgrop  29512  ausgrusgrb  29515  usgrstrrepe  29585  issubgr  29621  uhgrspansubgrlem  29640  usgrexi  29791  1hevtxdg1  29856  umgr2v2e  29875  zarcmplem  34271  ismeas  34589  omsval  34683  omscl  34685  omsf  34686  oms0  34687  carsgval  34693  omsmeas  34713  erdszelem3  35685  erdsze  35694  kur14  35708  iscvm  35751  mpstval  36027  mclsval  36055  mh-infprim2bi  37078  bj-imdirvallem  37844  pibp21  38081  heibor  38492  idlval  38684  igenval  38732  paddfval  40591  pclfvalN  40683  polfvalN  40698  docaffvalN  41915  docafvalN  41916  djaffvalN  41927  djafvalN  41928  dochffval  42143  dochfval  42144  djhffval  42190  djhfval  42191  lpolsetN  42276  lcdlss2N  42414  mzpclval  43476  dfac21  43813  islmodfg  43816  islssfg  43817  rfovd  44747  fsovrfovd  44755  gneispace2  44878  ismnu  44991  sge0val  47100  ismea  47185  psmeasure  47205  caragenval  47227  isome  47228  omeunile  47239  isomennd  47265  ovnval  47275  hspmbl  47363  isvonmbl  47372  afv2eq12d  47972  isisubgr  48647  isubgruhgr  48653  stgrfv  48738  stgrusgra  48744  gpgov  48827  gpgusgra  48842  lincop  49208  lcoop  49211  islininds  49246  ldepsnlinc  49308  isclatd  49781