Theorem pweqd 4559

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-pw 4544

This theorem is referenced by:  undefval  8220  pmvalg  8778  marypha1lem  9340  marypha1  9341  r1val3  9756  ackbij2lem2  10155  ackbij2lem3  10156  r1om  10159  isfin2  10210  hsmexlem8  10340  vdwmc  16943  hashbcval  16967  ismre  17546  mrcfval  17568  mrisval  17590  mreexexlemd  17604  brssc  17775  lubfval  18308  glbfval  18321  isclat  18460  issubmgm  18664  issubm  18765  issubg  19096  cntzfval  19289  lsmfval  19607  lsmpropd  19646  pj1fval  19663  issubrng  20518  issubrg  20542  rgspnval  20583  lssset  20922  lspfval  20962  lsppropd  21008  islbs  21066  sraval  21165  ocvfval  21659  isobs  21713  islinds  21802  aspval  21865  opsrval  22037  ply1frcl  22296  evls1fval  22297  basis1  22928  baspartn  22932  cldval  23001  ntrfval  23002  clsfval  23003  mretopd  23070  neifval  23077  lpfval  23116  cncls2  23251  iscnrm  23301  iscnrm2  23316  2ndcsep  23437  kgenval  23513  xkoval  23565  dfac14  23596  qtopval  23673  qtopval2  23674  isfbas  23807  trfbas2  23821  flimval  23941  elflim  23949  flimclslem  23962  fclsfnflim  24005  fclscmp  24008  tsmsfbas  24106  tsmsval2  24108  ustval  24181  utopval  24210  mopnfss  24421  setsmstopn  24456  met2ndc  24501  madeval  27841  elmade2  27867  istrkgb  28540  isuhgr  29146  isushgr  29147  isuhgrop  29156  uhgrun  29160  uhgrstrrepe  29164  isupgr  29170  upgrop  29180  isumgr  29181  upgrun  29204  umgrun  29206  isuspgr  29238  isusgr  29239  isuspgrop  29247  isusgrop  29248  ausgrusgrb  29251  usgrstrrepe  29321  issubgr  29357  uhgrspansubgrlem  29376  usgrexi  29527  1hevtxdg1  29593  umgr2v2e  29612  zarcmplem  34044  ismeas  34362  omsval  34456  omscl  34458  omsf  34459  oms0  34460  carsgval  34466  omsmeas  34486  erdszelem3  35394  erdsze  35403  kur14  35417  iscvm  35460  mpstval  35736  mclsval  35764  mh-infprim2bi  36748  bj-imdirvallem  37513  pibp21  37748  heibor  38159  idlval  38351  igenval  38399  paddfval  40260  pclfvalN  40352  polfvalN  40367  docaffvalN  41584  docafvalN  41585  djaffvalN  41596  djafvalN  41597  dochffval  41812  dochfval  41813  djhffval  41859  djhfval  41860  lpolsetN  41945  lcdlss2N  42083  mzpclval  43174  dfac21  43515  islmodfg  43518  islssfg  43519  rfovd  44449  fsovrfovd  44457  gneispace2  44580  ismnu  44709  sge0val  46815  ismea  46900  psmeasure  46920  caragenval  46942  isome  46943  omeunile  46954  isomennd  46980  ovnval  46990  hspmbl  47078  isvonmbl  47087  afv2eq12d  47678  isisubgr  48353  isubgruhgr  48359  stgrfv  48444  stgrusgra  48450  gpgov  48533  gpgusgra  48548  lincop  48899  lcoop  48902  islininds  48937  ldepsnlinc  48999  isclatd  49473