Theorem oveqd 7387

Description: Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveqd	⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Proof of Theorem oveqd

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq 7376	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Syntax hints:   → wi 4   = wceq 1542  (class class class)co 7370

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 3444  df-ss 3920  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373

This theorem is referenced by:  oveq123d  7391  oveqdr  7398  csbov  7415  csbov12g  7416  ovmpodxf  7520  oprssov  7539  2mpo0  7619  ofeqd  7636  mptmpoopabbrd  8036  mptmpoopabbrdOLD  8037  mptmpoopabovd  8038  el2mpocsbcl  8039  fnmpoovd  8041  frecseq123  8236  ruclem1  16170  vdwapval  16915  vdwapid1  16917  vdwmc2  16921  vdwpc  16922  vdwlem5  16927  vdwlem8  16930  vdwlem13  16935  prdsval  17389  prdsdsval2  17418  pwsplusgval  17425  pwsmulrval  17426  pwsvscafval  17429  imasval  17446  iscat  17609  iscatd  17610  catidex  17611  catideu  17612  cidfval  17613  cidval  17614  catidd  17617  iscatd2  17618  catlid  17620  catrid  17621  homffval  17627  homfeqd  17632  homfeqval  17634  comfffval  17635  comffval  17636  comfeq  17643  comfeqd  17644  comfeqval  17645  catpropd  17646  oppcval  17650  oppcco  17654  monfval  17670  ismon  17671  oppcmon  17676  oppcepi  17677  sectffval  17688  sectfval  17689  invffval  17696  isoval  17703  dfiso2  17710  isofn  17713  invisoinvl  17728  invcoisoid  17730  isocoinvid  17731  issubc  17773  issubc3  17787  isfunc  17802  cofuval  17820  cofuval2  17825  funcres  17834  funcres2b  17835  funcres2  17836  idfusubc  17838  funcres2c  17841  isfull  17850  isfth  17854  fullres2c  17879  natfval  17887  isnat  17888  fucval  17899  fucco  17903  fucpropd  17918  initoval  17931  termoval  17932  homarcl  17966  coafval  18002  resssetc  18030  resscatc  18047  catciso  18049  xpcval  18114  1stfval  18128  2ndfval  18131  prfval  18136  prfcl  18140  evlfval  18154  curfval  18160  curf1cl  18165  curfcl  18169  uncf1  18173  uncf2  18174  diag12  18181  diag2  18182  curf2ndf  18184  hofval  18189  hof1  18191  hof2fval  18192  hofcl  18196  yon12  18202  yon2  18203  hofpropd  18204  joinval  18312  meetval  18326  isdlat  18459  plusffval  18585  ismgmd  18591  issstrmgm  18592  grpidval  18600  grpidd  18610  gsumvalx  18615  gsumpropd  18617  gsumress  18621  ismgmhm  18635  issubmgm  18641  resmgmhm  18650  resmgmhm2  18651  resmgmhm2b  18652  issgrpd  18669  ismndd  18695  issubmnd  18700  submnd0  18702  ismhm  18724  issubm  18742  resmhm  18759  resmhm2  18760  resmhm2b  18761  mhmimalem  18763  isgrp  18886  isgrpd2e  18902  grpidd2  18924  grpinvfval  18925  grpinvfvalALT  18926  imasgrp2  19002  imasgrp  19003  subg0  19079  subginv  19080  subgcl  19083  issubgrpd2  19089  isnsg  19101  isghm  19161  isghmOLD  19162  resghm  19178  isga  19237  subgga  19246  gasubg  19248  cntzfval  19266  resscntz  19279  odfval  19478  odfvalALT  19479  gexval  19524  lsmfval  19584  lsmvalx  19585  oppglsm  19588  subglsm  19619  pj1fval  19640  efgtval  19669  iscmn  19735  iscmnd  19740  submcmn2  19785  imasabl  19822  iscyg  19825  cycsubmcmn  19835  isomnd  20069  submomnd  20078  prdsmgp  20103  rngpropd  20126  ringurd  20137  issrg  20140  isring  20189  ringidss  20229  mulgass3  20306  dvdsrval  20314  rdivmuldivd  20366  isirred  20372  rnghmval  20393  islring  20490  lringuplu  20494  subrngmcl  20507  subrg1  20532  subrgdvds  20536  subrguss  20537  subrginv  20538  subrgdv  20539  subrgunit  20540  subrgugrp  20541  rnghmresel  20570  rngchom  20573  rngcco  20577  rnghmsubcsetclem1  20581  rhmresel  20599  ringchom  20602  ringcco  20606  rhmsubcsetclem1  20610  rhmsubcrngclem1  20616  rrgval  20647  isdrngd  20715  isdrngrd  20716  isdrngdOLD  20717  isdrngrdOLD  20718  abvfval  20760  isabvd  20762  issrngd  20805  isorng  20811  suborng  20826  islmod  20832  islmodd  20834  scaffval  20848  lmodpropd  20893  lssset  20901  islssd  20903  prdslmodd  20937  islmhm  20996  reslmhm  21021  reslmhm2  21022  reslmhm2b  21023  islbs  21045  rlmvneg  21175  rnglidlmmgm  21217  rnglidlmsgrp  21218  rnglidlrng  21219  rngqiprngghmlem3  21261  rngqiprngimfolem  21262  rngqiprnglinlem1  21263  rngqiprngimf1  21272  rngqiprnglin  21274  rng2idl1cntr  21277  rngqiprngfulem5  21287  irinitoringc  21451  isphl  21600  ipffval  21620  isphld  21626  phssipval  21629  phssip  21630  phlssphl  21631  ocvfval  21638  isobs  21692  frlmplusgval  21736  frlmsubgval  21737  frlmvscafval  21738  frlmip  21750  frlmipval  21751  frlmup1  21770  lsslindf  21802  isassa  21828  isassad  21837  sraassab  21840  assamulgscmlem2  21873  psrval  21888  resspsradd  21947  resspsrmul  21948  resspsrvsca  21949  mplmon2mul  22041  ply1coe  22259  ply1chr  22267  lply1binomsc  22272  evl1expd  22306  evl1scvarpw  22324  asclply1subcl  22335  mamufval  22353  matplusg2  22388  matvsca2  22389  matplusgcell  22394  matsubgcell  22395  matinvgcell  22396  matvscacell  22397  matmulcell  22406  mpomatmul  22407  mat1  22408  mattposm  22420  mat1dimmul  22437  dmatmul  22458  dmatcrng  22463  scmataddcl  22477  scmatsubcl  22478  scmatcrng  22482  smatvscl  22485  scmatghm  22494  scmatmhm  22495  mvmulfval  22503  ma1repveval  22532  mdetrlin  22563  mdetrsca  22564  mdetmul  22584  madurid  22605  minmar1cl  22612  smadiadetglem1  22632  smadiadetr  22636  matinv  22638  slesolinv  22641  slesolinvbi  22642  cramerimplem3  22646  cpmatacl  22677  mat2pmatghm  22691  decpmatmullem  22732  decpmatmul  22733  pmatcollpw1lem1  22735  pmatcollpw2lem  22738  pmatcollpwlem  22741  pmatcollpw3lem  22744  mply1topmatval  22765  mp2pm2mplem1  22767  mp2pm2mplem4  22770  mp2pm2mplem5  22771  mp2pm2mp  22772  chpmat1d  22797  chpscmatgsummon  22806  chfacfpmmulgsum2  22826  xkocnv  23775  submtmd  24065  prdsdsf  24328  ressprdsds  24332  blfvalps  24344  prdsxmslem2  24490  tmsxpsval  24499  ngpds  24565  sgrimval  24593  subgngp  24596  tngngp  24615  tngngp3  24617  isnlm  24636  lssnlm  24662  isphtpy  24953  isphtpc  24966  pi1cpbl  25017  pi1addf  25020  pi1addval  25021  pi1grplem  25022  clmsub  25053  clmvsass  25062  clmvsdir  25064  isclmp  25070  cvsdiv  25105  iscph  25143  cphdir  25178  cphdi  25179  cph2di  25180  cph2subdi  25183  cphass  25184  tcphval  25191  ipcau2  25207  tcphcphlem1  25208  tcphcphlem2  25209  cphsscph  25224  caufval  25248  rrxip  25363  rrxvsca  25367  rrxplusgvscavalb  25368  rrxdsfival  25386  ehleudisval  25392  dvlip2  25973  q1pval  26133  r1pval  26136  dvntaylp  26352  efabl  26532  efsubm  26533  dchrmul  27232  seqseq123d  28299  istrkgc  28543  istrkgb  28544  istrkgcb  28545  istrkge  28546  istrkgl  28547  istrkgld  28548  iscgrg  28602  isismt  28624  tglngval  28641  legval  28674  ishlg  28692  mirval  28745  israg  28787  ishpg  28849  lmif  28875  islmib  28877  isinag  28928  ttgval  28965  wksonproplem  29794  wspthsnon  29943  iswwlksnon  29944  iswspthsnon  29947  isconngr  30282  isconngr1  30283  grpodivval  30629  dipfval  30796  ipval  30797  sspgval  30823  sspsval  30825  lnoval  30846  ajfval  30903  dipdir  30936  dipass  30939  htth  31012  ressmulgnn0d  33144  inftmrel  33280  isinftm  33281  isslmd  33302  elrgspnlem1  33342  erlval  33358  rlocval  33359  rlocaddval  33368  rlocmulval  33369  subrdom  33385  resv1r  33438  lsmidllsp  33499  idlinsubrg  33530  prmidlval  33536  idlsrgval  33602  idlsrg0g  33605  rprmval  33615  ressply1evls1  33664  vietalem  33762  drgextlsp  33777  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  extdg1id  33850  fldextrspunlsplem  33857  fldextrspunlsp  33858  extdgfialglem1  33876  extdgfialglem2  33877  algextdeglem8  33908  smatlem  33981  submatminr1  33994  metidval  34074  pstmval  34079  pstmfval  34080  zlm0  34144  zlm1  34145  sitmval  34533  breprexp  34817  istrkg2d  34850  afsval  34855  mclsrcl  35783  mppsval  35794  bj-endval  37597  matunitlindflem2  37897  istotbnd  38049  isbnd  38060  rrnequiv  38115  isrngo  38177  rngohomval  38244  idlval  38293  pridlval  38313  lflset  39464  islfld  39467  ldualvadd  39534  ldualsmul  39540  ldualvs  39542  isopos  39585  cmtfvalN  39615  iscvlat  39728  ishlat1  39757  lineset  40143  psubspset  40149  paddfval  40202  paddval  40203  ltrnfset  40522  trnfsetN  40560  trlfset  40565  tgrpov  41153  erngplus  41208  erngmul  41211  erngplus-rN  41216  erngmul-rN  41219  erngdvlem3  41395  erngdvlem4  41396  erng0g  41399  erngdvlem3-rN  41403  erngdvlem4-rN  41404  dvaplusg  41414  dvamulr  41417  dvavadd  41420  dvavsca  41422  dvalveclem  41430  dvhmulr  41491  dvhfvadd  41496  dvhvadd  41497  dvhopvadd2  41499  dvhvaddcl  41500  dvhvaddcomN  41501  dvhvsca  41506  dvhlveclem  41513  dvh0g  41516  djavalN  41540  diblsmopel  41576  dicvaddcl  41595  cdlemn6  41607  dihffval  41635  dihopelvalcpre  41653  djhval  41803  lcdvaddval  42003  lcdsmul  42007  lcdvsval  42009  lcdlkreq2N  42028  hvmapffval  42163  hvmapfval  42164  hdmap1fval  42201  hgmapffval  42290  hgmapfval  42291  hgmapadd  42299  hlhilipval  42354  hlhilhillem  42365  isprimroot  42492  aks6d1c1p4  42510  idomnnzpownz  42531  aks6d1c5lem1  42535  aks6d1c5lem3  42536  aks6d1c5lem2  42537  aks5lem3a  42588  unitscyglem5  42598  rhmpsr1  42950  selvvvval  42972  mhphf2  42985  prjspval  42990  prjspner1  43013  sn-isghm  43060  mnringvald  44598  ioorrnopnlem  46691  hoidmvval0b  46977  hoidmvlelem2  46983  hoidmvlelem3  46984  hoidmvle  46987  ovnhoi  46990  hoiqssbl  47012  hspmbllem2  47014  vonioo  47069  vonicc  47072  zlidlring  48623  uzlidlring  48624  ovmpordxf  48728  lincop  48797  lincval  48798  lincsum  48818  lincscm  48819  lmod1lem2  48877  lmod1lem3  48878  lmod1lem4  48879  ldepsnlinc  48897  lines  49120  line  49121  rrxlines  49122  rrxline  49123  spheres  49135  fvconstr  49250  fvconstrn0  49251  fvconstr2  49252  catprs  49399  sectrcl2  49411  invrcl2  49413  invfn  49418  isorcl2  49422  sectpropdlem  49424  invpropdlem  49426  isopropdlem  49428  cicpropdlem  49437  iinfconstbas  49454  nelsubclem  49455  nelsubc3lem  49458  ssccatid  49460  resccatlem  49461  cofu2a  49483  cofid2a  49501  cofid2  49503  cofidf2a  49505  cofidf2  49508  oppf2  49528  upfval  49564  upfval2  49565  upfval3  49566  upeu3  49583  upeu4  49584  oppcup3  49597  natoppfb  49619  swapfval  49650  swapf2a  49659  1stfpropd  49678  2ndfpropd  49679  cofuswapf2  49683  tposcurf12  49686  tposcurf2  49688  tposcurf2cl  49690  fucofvalg  49706  fuco11b  49725  fuco23a  49740  precofval3  49759  prcofpropd  49767  catcrcl2  49784  opf12  49792  fucoppcco  49797  thincmod  49818  isthincd2lem2  49823  isthincd  49824  dfinito4  49889  mndtcco2  49974  mndtccatid  49975  oppgoppchom  49978  oppgoppcco  49979  grptcmon  49981  grptcepi  49982  2arwcatlem2  49984  2arwcatlem3  49985  2arwcatlem4  49986  2arwcat  49988  lanrcl  50009  ranrcl  50010  rellan  50011  relran  50012  concom  50051  coccom  50052