Theorem pweqd 4549

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

Syntax hints:   → wi 4   = wceq 1539  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  undefval  8063  pmvalg  8584  marypha1lem  9122  marypha1  9123  r1val3  9527  ackbij2lem2  9927  ackbij2lem3  9928  r1om  9931  isfin2  9981  hsmexlem8  10111  vdwmc  16607  hashbcval  16631  ismre  17216  mrcfval  17234  mrisval  17256  mreexexlemd  17270  brssc  17443  lubfval  17983  glbfval  17996  isclat  18133  issubm  18357  issubg  18670  cntzfval  18841  lsmfval  19158  lsmpropd  19198  pj1fval  19215  issubrg  19939  lssset  20110  lspfval  20150  lsppropd  20195  islbs  20253  sraval  20353  ocvfval  20783  isobs  20837  islinds  20926  aspval  20987  opsrval  21157  ply1frcl  21394  evls1fval  21395  basis1  22008  baspartn  22012  cldval  22082  ntrfval  22083  clsfval  22084  mretopd  22151  neifval  22158  lpfval  22197  cncls2  22332  iscnrm  22382  iscnrm2  22397  2ndcsep  22518  kgenval  22594  xkoval  22646  dfac14  22677  qtopval  22754  qtopval2  22755  isfbas  22888  trfbas2  22902  flimval  23022  elflim  23030  flimclslem  23043  fclsfnflim  23086  fclscmp  23089  tsmsfbas  23187  tsmsval2  23189  ustval  23262  utopval  23292  mopnfss  23504  setsmstopn  23539  met2ndc  23585  istrkgb  26720  isuhgr  27333  isushgr  27334  isuhgrop  27343  uhgrun  27347  uhgrstrrepe  27351  isupgr  27357  upgrop  27367  isumgr  27368  upgrun  27391  umgrun  27393  isuspgr  27425  isusgr  27426  isuspgrop  27434  isusgrop  27435  ausgrusgrb  27438  usgrstrrepe  27505  issubgr  27541  uhgrspansubgrlem  27560  usgrexi  27711  1hevtxdg1  27776  umgr2v2e  27795  zarcmplem  31733  ismeas  32067  omsval  32160  omscl  32162  omsf  32163  oms0  32164  carsgval  32170  omsmeas  32190  erdszelem3  33055  erdsze  33064  kur14  33078  iscvm  33121  mpstval  33397  mclsval  33425  madeval  33963  elmade2  33979  bj-imdirvallem  35278  pibp21  35513  heibor  35906  idlval  36098  igenval  36146  paddfval  37738  pclfvalN  37830  polfvalN  37845  docaffvalN  39062  docafvalN  39063  djaffvalN  39074  djafvalN  39075  dochffval  39290  dochfval  39291  djhffval  39337  djhfval  39338  lpolsetN  39423  lcdlss2N  39561  mzpclval  40463  dfac21  40807  islmodfg  40810  islssfg  40811  rgspnval  40909  rfovd  41498  fsovrfovd  41506  gneispace2  41631  ismnu  41768  sge0val  43794  ismea  43879  psmeasure  43899  caragenval  43921  isome  43922  omeunile  43933  isomennd  43959  ovnval  43969  hspmbl  44057  isvonmbl  44066  afv2eq12d  44594  issubmgm  45231  lincop  45637  lcoop  45640  islininds  45675  ldepsnlinc  45737  isclatd  46157