Theorem pweqd 4113

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

Syntax hints:   → wi 4   = wceq 1475  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  undefval  7289  pmvalg  7755  marypha1lem  8222  marypha1  8223  r1val3  8584  ackbij1lem5  8929  ackbij2lem2  8945  ackbij2lem3  8946  r1om  8949  isfin2  8999  hsmexlem8  9129  vdwmc  15520  hashbcval  15544  ismre  16073  mrcfval  16091  mrisval  16113  mreexexlemd  16127  brssc  16297  lubfval  16801  glbfval  16814  isclat  16932  issubm  17170  issubg  17417  cntzfval  17576  symgval  17622  lsmfval  17876  lsmpropd  17913  pj1fval  17930  issubrg  18603  lssset  18755  lspfval  18794  lsppropd  18839  islbs  18897  sraval  18997  aspval  19149  opsrval  19295  ply1frcl  19504  evls1fval  19505  ocvfval  19829  isobs  19883  islinds  19967  basis1  20565  baspartn  20569  cldval  20637  ntrfval  20638  clsfval  20639  mretopd  20706  neifval  20713  lpfval  20752  cncls2  20887  iscnrm  20937  iscnrm2  20952  2ndcsep  21072  kgenval  21148  xkoval  21200  dfac14  21231  qtopval  21308  qtopval2  21309  isfbas  21443  trfbas2  21457  flimval  21577  elflim  21585  flimclslem  21598  fclsfnflim  21641  fclscmp  21644  tsmsfbas  21741  tsmsval2  21743  ustval  21816  utopval  21846  mopnfss  22058  setsmstopn  22093  met2ndc  22138  istrkgb  25154  isuhgr  25726  isushgr  25727  isuhgrop  25736  uhgrun  25740  uhgrstrrepe  25745  isupgr  25751  isumgr  25761  upgrun  25784  umgrun  25786  isumgra  25844  isuslgra  25872  isusgra  25873  edgss  25881  ismeas  29589  omsval  29682  omscl  29684  omsf  29685  oms0  29686  carsgval  29692  omsmeas  29712  erdszelem3  30429  erdsze  30438  kur14  30452  iscvm  30495  mpstval  30686  mclsval  30714  heibor  32790  idlval  32982  igenval  33030  paddfval  34101  pclfvalN  34193  polfvalN  34208  docaffvalN  35428  docafvalN  35429  djaffvalN  35440  djafvalN  35441  dochffval  35656  dochfval  35657  djhffval  35703  djhfval  35704  lpolsetN  35789  lcdlss2N  35927  mzpclval  36306  dfac21  36654  islmodfg  36657  islssfg  36658  rgspnval  36757  rfovd  37315  fsovrfovd  37323  gneispace2  37450  sge0val  39259  ismea  39344  psmeasure  39364  caragenval  39383  isome  39384  omeunile  39395  isomennd  39421  ovnval  39431  hspmbl  39519  isvonmbl  39528  isuspgr  40382  isusgr  40383  isusgrop  40392  ausgrusgrb  40395  issubgr  40495  uhgrspansubgrlem  40514  usgrexi  40661  1hevtxdg1  40721  umgr2v2e  40741  issubmgm  41579  lincop  41991  lcoop  41994  islininds  42029  ldepsnlinc  42091