MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveqd Structured version   Visualization version   GIF version

Theorem oveqd 6707
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
StepHypRef Expression
1 oveq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 oveq 6696 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  (class class class)co 6690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  oveq123d  6711  oveqdr  6714  csbov  6728  csbov12g  6729  ovmpt2dxf  6828  oprssov  6845  2mpt20  6924  ofeq  6941  mptmpt2opabbrd  7293  mptmpt2opabovd  7294  el2mpt2csbcl  7295  fnmpt2ovd  7297  ruclem1  15004  vdwapval  15724  vdwapid1  15726  vdwmc2  15730  vdwpc  15731  vdwlem5  15736  vdwlem8  15739  vdwlem13  15744  prdsval  16162  prdsdsval2  16191  pwsplusgval  16197  pwsmulrval  16198  pwsvscafval  16201  imasval  16218  iscat  16380  iscatd  16381  catidex  16382  catideu  16383  cidfval  16384  cidval  16385  catidd  16388  iscatd2  16389  catlid  16391  catrid  16392  homffval  16397  homfeqd  16402  homfeqval  16404  comfffval  16405  comffval  16406  comfeq  16413  comfeqd  16414  comfeqval  16415  catpropd  16416  oppcval  16420  oppcco  16424  monfval  16439  ismon  16440  oppcmon  16445  oppcepi  16446  sectffval  16457  sectfval  16458  invffval  16465  isoval  16472  dfiso2  16479  isofn  16482  invisoinvl  16497  invcoisoid  16499  isocoinvid  16500  issubc  16542  issubc3  16556  isfunc  16571  cofuval  16589  cofuval2  16594  funcres  16603  funcres2b  16604  funcres2  16605  funcres2c  16608  isfull  16617  isfth  16621  fullres2c  16646  natfval  16653  isnat  16654  fucval  16665  fucco  16669  fucpropd  16684  initoval  16694  termoval  16695  homarcl  16725  coafval  16761  resssetc  16789  resscatc  16802  catciso  16804  xpcval  16864  1stfval  16878  2ndfval  16881  prfval  16886  prfcl  16890  evlfval  16904  curfval  16910  curf1cl  16915  curfcl  16919  uncf1  16923  uncf2  16924  diag12  16931  diag2  16932  curf2ndf  16934  hofval  16939  hof1  16941  hof2fval  16942  hofcl  16946  yon12  16952  yon2  16953  hofpropd  16954  joinval  17052  meetval  17066  isdlat  17240  plusffval  17294  issstrmgm  17299  grpidval  17307  grpidd  17315  gsumvalx  17317  gsumpropd  17319  gsumress  17323  ismndd  17360  issubmnd  17365  submnd0  17367  ismhm  17384  issubm  17394  resmhm  17406  resmhm2  17407  resmhm2b  17408  isgrp  17475  isgrpd2e  17488  grpidd2  17506  grpinvfval  17507  imasgrp2  17577  imasgrp  17578  subg0  17647  subginv  17648  subgcl  17651  issubgrpd2  17657  isnsg  17670  isghm  17707  resghm  17723  isga  17770  subgga  17779  gasubg  17781  cntzfval  17799  resscntz  17810  odfval  17998  gexval  18039  lsmfval  18099  lsmvalx  18100  oppglsm  18103  subglsm  18132  pj1fval  18153  efgtval  18182  iscmn  18246  iscmnd  18251  submcmn2  18290  iscyg  18327  issrg  18553  isring  18597  ringidss  18623  prdsmgp  18656  mulgass3  18683  dvdsrval  18691  isirred  18745  isdrngd  18820  isdrngrd  18821  subrg1  18838  subrgmcl  18840  subrgdvds  18842  subrguss  18843  subrginv  18844  subrgdv  18845  subrgunit  18846  subrgugrp  18847  abvfval  18866  isabvd  18868  issrngd  18909  islmod  18915  islmodd  18917  scaffval  18929  lmodpropd  18974  lssset  18982  islssd  18984  prdslmodd  19017  islmhm  19075  reslmhm  19100  reslmhm2  19101  reslmhm2b  19102  islbs  19124  rlmvneg  19255  rrgval  19335  isassa  19363  isassad  19371  assamulgscmlem2  19397  psrval  19410  resspsradd  19464  resspsrmul  19465  resspsrvsca  19466  mplmon2mul  19549  ply1coe  19714  lply1binomsc  19725  evl1expd  19757  evl1scvarpw  19775  isphl  20021  ipffval  20041  isphld  20047  phssipval  20050  phssip  20051  ocvfval  20058  isobs  20112  frlmplusgval  20155  frlmsubgval  20156  frlmvscafval  20157  frlmip  20165  frlmipval  20166  frlmup1  20185  lsslindf  20217  mamufval  20239  matplusg2  20281  matvsca2  20282  matplusgcell  20287  matsubgcell  20288  matinvgcell  20289  matvscacell  20290  matmulcell  20299  mpt2matmul  20300  mat1  20301  mattposm  20313  mat1dimmul  20330  dmatmul  20351  dmatcrng  20356  scmataddcl  20370  scmatsubcl  20371  scmatcrng  20375  smatvscl  20378  scmatghm  20387  scmatmhm  20388  mvmulfval  20396  ma1repveval  20425  mdetrlin  20456  mdetrsca  20457  mdetmul  20477  madurid  20498  minmar1cl  20505  smadiadetglem1  20525  smadiadetr  20529  matinv  20531  slesolinv  20534  slesolinvbi  20535  cramerimplem3  20539  cpmatacl  20569  mat2pmatghm  20583  decpmatmullem  20624  decpmatmul  20625  pmatcollpw1lem1  20627  pmatcollpw2lem  20630  pmatcollpwlem  20633  pmatcollpw3lem  20636  mply1topmatval  20657  mp2pm2mplem1  20659  mp2pm2mplem4  20662  mp2pm2mplem5  20663  mp2pm2mp  20664  chpmat1d  20689  chpscmatgsummon  20698  chfacfpmmulgsum2  20718  xkocnv  21665  submtmd  21955  prdsdsf  22219  ressprdsds  22223  blfvalps  22235  prdsxmslem2  22381  tmsxpsval  22390  ngpds  22455  sgrimval  22483  subgngp  22486  tngngp  22505  tngngp3  22507  isnlm  22526  lssnlm  22552  isphtpy  22827  isphtpc  22840  pi1cpbl  22890  pi1addf  22893  pi1addval  22894  pi1grplem  22895  clmsub  22926  clmvsass  22935  clmvsdir  22937  isclmp  22943  cvsi  22976  cvsdiv  22978  iscph  23016  cphdir  23051  cphdi  23052  cph2di  23053  cph2subdi  23056  cphass  23057  tchval  23063  ipcau2  23079  tchcphlem1  23080  tchcphlem2  23081  caufval  23119  rrxip  23224  dvlip2  23803  q1pval  23958  r1pval  23961  dvntaylp  24170  efabl  24341  efsubm  24342  dchrmul  25018  istrkgc  25398  istrkgb  25399  istrkgcb  25400  istrkge  25401  istrkgl  25402  istrkgld  25403  iscgrg  25452  isismt  25474  tglngval  25491  legval  25524  ishlg  25542  mirval  25595  israg  25637  ishpg  25696  lmif  25722  islmib  25724  isinag  25774  ttgval  25800  wksonproplem  26657  wspthsnon  26801  iswwlksnon  26802  iswwlksnonOLD  26803  iswspthsnon  26806  iswspthsnonOLD  26807  isconngr  27167  isconngr1  27168  grpodivval  27517  dipfval  27685  ipval  27686  sspgval  27712  sspsval  27714  lnoval  27735  ajfval  27792  dipdir  27825  dipass  27828  htth  27903  isomnd  29829  submomnd  29838  inftmrel  29862  isinftm  29863  isslmd  29883  rngurd  29916  rdivmuldivd  29919  isorng  29927  suborng  29943  resv1r  29965  smatlem  29991  submatminr1  30004  metidval  30061  pstmval  30066  pstmfval  30067  zlm0  30134  zlm1  30135  sitmval  30539  breprexp  30839  istrkg2d  30872  afsval  30877  mclsrcl  31584  mppsval  31595  frecseq123  31902  matunitlindflem2  33536  istotbnd  33698  isbnd  33709  rrnequiv  33764  isrngo  33826  rngohomval  33893  idlval  33942  pridlval  33962  lflset  34664  islfld  34667  ldualvadd  34734  ldualsmul  34740  ldualvs  34742  isopos  34785  cmtfvalN  34815  iscvlat  34928  ishlat1  34957  lineset  35342  psubspset  35348  paddfval  35401  paddval  35402  ltrnfset  35721  trnfsetN  35760  trlfset  35765  tgrpov  36353  erngplus  36408  erngmul  36411  erngplus-rN  36416  erngmul-rN  36419  erngdvlem3  36595  erngdvlem4  36596  erng0g  36599  erngdvlem3-rN  36603  erngdvlem4-rN  36604  dvaplusg  36614  dvamulr  36617  dvavadd  36620  dvavsca  36622  dvalveclem  36631  dvhmulr  36692  dvhfvadd  36697  dvhvadd  36698  dvhopvadd2  36700  dvhvaddcl  36701  dvhvaddcomN  36702  dvhvsca  36707  dvhlveclem  36714  dvh0g  36717  djavalN  36741  diblsmopel  36777  dicvaddcl  36796  cdlemn6  36808  dihffval  36836  dihopelvalcpre  36854  djhval  37004  lcdvaddval  37204  lcdsmul  37208  lcdvsval  37210  lcdlkreq2N  37229  hvmapffval  37364  hvmapfval  37365  hdmap1fval  37403  hgmapffval  37494  hgmapfval  37495  hgmapadd  37503  hlhilipval  37558  hlhilhillem  37569  ioorrnopnlem  40842  hoidmvval0b  41125  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvle  41135  ovnhoi  41138  hoiqssbl  41160  hspmbllem2  41162  vonioo  41217  vonicc  41220  ismgmd  42101  ismgmhm  42108  issubmgm  42114  resmgmhm  42123  resmgmhm2  42124  resmgmhm2b  42125  idfusubc  42191  rnghmval  42216  lidlmsgrp  42251  lidlrng  42252  zlidlring  42253  uzlidlring  42254  rnghmresel  42289  rngchom  42292  rngcco  42296  rnghmsubcsetclem1  42300  rhmresel  42335  ringchom  42338  ringcco  42342  rhmsubcsetclem1  42346  rhmsubcrngclem1  42352  irinitoringc  42394  ovmpt2rdxf  42442  lincop  42522  lincval  42523  lincsum  42543  lincscm  42544  lmod1lem2  42602  lmod1lem3  42603  lmod1lem4  42604  ldepsnlinc  42622
  Copyright terms: Public domain W3C validator