Theorem pweqd 4558

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

Syntax hints:   → wi 4   = wceq 1542  𝒫 cpw 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-pw 4543

This theorem is referenced by:  undefval  8226  pmvalg  8784  marypha1lem  9346  marypha1  9347  r1val3  9762  ackbij2lem2  10161  ackbij2lem3  10162  r1om  10165  isfin2  10216  hsmexlem8  10346  vdwmc  16949  hashbcval  16973  ismre  17552  mrcfval  17574  mrisval  17596  mreexexlemd  17610  brssc  17781  lubfval  18314  glbfval  18327  isclat  18466  issubmgm  18670  issubm  18771  issubg  19102  cntzfval  19295  lsmfval  19613  lsmpropd  19652  pj1fval  19669  issubrng  20524  issubrg  20548  rgspnval  20589  lssset  20928  lspfval  20968  lsppropd  21013  islbs  21071  sraval  21170  ocvfval  21646  isobs  21700  islinds  21789  aspval  21852  opsrval  22024  ply1frcl  22283  evls1fval  22284  basis1  22915  baspartn  22919  cldval  22988  ntrfval  22989  clsfval  22990  mretopd  23057  neifval  23064  lpfval  23103  cncls2  23238  iscnrm  23288  iscnrm2  23303  2ndcsep  23424  kgenval  23500  xkoval  23552  dfac14  23583  qtopval  23660  qtopval2  23661  isfbas  23794  trfbas2  23808  flimval  23928  elflim  23936  flimclslem  23949  fclsfnflim  23992  fclscmp  23995  tsmsfbas  24093  tsmsval2  24095  ustval  24168  utopval  24197  mopnfss  24408  setsmstopn  24443  met2ndc  24488  madeval  27824  elmade2  27850  istrkgb  28523  isuhgr  29129  isushgr  29130  isuhgrop  29139  uhgrun  29143  uhgrstrrepe  29147  isupgr  29153  upgrop  29163  isumgr  29164  upgrun  29187  umgrun  29189  isuspgr  29221  isusgr  29222  isuspgrop  29230  isusgrop  29231  ausgrusgrb  29234  usgrstrrepe  29304  issubgr  29340  uhgrspansubgrlem  29359  usgrexi  29510  1hevtxdg1  29575  umgr2v2e  29594  zarcmplem  34025  ismeas  34343  omsval  34437  omscl  34439  omsf  34440  oms0  34441  carsgval  34447  omsmeas  34467  erdszelem3  35375  erdsze  35384  kur14  35398  iscvm  35441  mpstval  35717  mclsval  35745  mh-infprim2bi  36729  bj-imdirvallem  37494  pibp21  37731  heibor  38142  idlval  38334  igenval  38382  paddfval  40243  pclfvalN  40335  polfvalN  40350  docaffvalN  41567  docafvalN  41568  djaffvalN  41579  djafvalN  41580  dochffval  41795  dochfval  41796  djhffval  41842  djhfval  41843  lpolsetN  41928  lcdlss2N  42066  mzpclval  43157  dfac21  43494  islmodfg  43497  islssfg  43498  rfovd  44428  fsovrfovd  44436  gneispace2  44559  ismnu  44688  sge0val  46794  ismea  46879  psmeasure  46899  caragenval  46921  isome  46922  omeunile  46933  isomennd  46959  ovnval  46969  hspmbl  47057  isvonmbl  47066  afv2eq12d  47663  isisubgr  48338  isubgruhgr  48344  stgrfv  48429  stgrusgra  48435  gpgov  48518  gpgusgra  48533  lincop  48884  lcoop  48887  islininds  48922  ldepsnlinc  48984  isclatd  49458