Theorem pweqd 4572

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

Syntax hints:   → wi 4   = wceq 1560  𝒫 cpw 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-pw 4557

This theorem is referenced by:  undefval  8257  pmvalg  8818  marypha1lem  9379  marypha1  9380  r1val3  9796  ackbij2lem2  10195  ackbij2lem3  10196  r1om  10199  isfin2  10251  hsmexlem8  10381  vdwmc  17014  hashbcval  17038  ismre  17618  mrcfval  17640  mrisval  17662  mreexexlemd  17676  brssc  17847  lubfval  18380  glbfval  18393  isclat  18532  issubmgm  18736  issubm  18837  issubg  19168  cntzfval  19360  lsmfval  19678  lsmpropd  19717  pj1fval  19734  issubrng  20597  issubrg  20621  rgspnval  20662  lssset  21000  lspfval  21040  lsppropd  21085  islbs  21143  sraval  21242  ocvfval  21718  isobs  21772  islinds  21861  aspval  21924  opsrval  22099  ply1frcl  22381  evls1fval  22382  basis1  23010  baspartn  23014  cldval  23083  ntrfval  23084  clsfval  23085  mretopd  23152  neifval  23159  lpfval  23198  cncls2  23333  iscnrm  23383  iscnrm2  23398  2ndcsep  23519  kgenval  23595  xkoval  23647  dfac14  23678  qtopval  23755  qtopval2  23756  isfbas  23889  trfbas2  23903  flimval  24023  elflim  24031  flimclslem  24044  fclsfnflim  24087  fclscmp  24090  tsmsfbas  24188  tsmsval2  24190  ustval  24263  utopval  24292  mopnfss  24503  setsmstopn  24538  met2ndc  24583  madeval  27925  elmade2  27951  istrkgb  28624  isuhgr  29261  isushgr  29262  isuhgrop  29271  uhgrun  29275  uhgrstrrepe  29279  isupgr  29285  upgrop  29295  isumgr  29296  upgrun  29319  umgrun  29321  isuspgr  29353  isusgr  29354  isuspgrop  29362  isusgrop  29363  ausgrusgrb  29366  usgrstrrepe  29436  issubgr  29472  uhgrspansubgrlem  29491  usgrexi  29642  1hevtxdg1  29707  umgr2v2e  29726  zarcmplem  34178  ismeas  34496  omsval  34590  omscl  34592  omsf  34593  oms0  34594  carsgval  34600  omsmeas  34620  erdszelem3  35543  erdsze  35552  kur14  35566  iscvm  35609  mpstval  35885  mclsval  35913  mh-infprim2bi  36907  bj-imdirvallem  37672  pibp21  37909  heibor  38320  idlval  38512  igenval  38560  paddfval  40421  pclfvalN  40513  polfvalN  40528  docaffvalN  41745  docafvalN  41746  djaffvalN  41757  djafvalN  41758  dochffval  41973  dochfval  41974  djhffval  42020  djhfval  42021  lpolsetN  42106  lcdlss2N  42244  mzpclval  43306  dfac21  43643  islmodfg  43646  islssfg  43647  rfovd  44577  fsovrfovd  44585  gneispace2  44708  ismnu  44837  sge0val  46940  ismea  47025  psmeasure  47045  caragenval  47067  isome  47068  omeunile  47079  isomennd  47105  ovnval  47115  hspmbl  47203  isvonmbl  47212  afv2eq12d  47809  isisubgr  48484  isubgruhgr  48490  stgrfv  48575  stgrusgra  48581  gpgov  48664  gpgusgra  48679  lincop  49030  lcoop  49033  islininds  49068  ldepsnlinc  49130  isclatd  49604