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

Theorem oveqd 6900
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 6889 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  (class class class)co 6883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rex 3113  df-uni 4642  df-br 4856  df-iota 6073  df-fv 6118  df-ov 6886
This theorem is referenced by:  oveq123d  6904  oveqdr  6911  csbov  6925  csbov12g  6926  ovmpt2dxf  7025  oprssov  7042  2mpt20  7121  ofeq  7138  mptmpt2opabbrd  7490  mptmpt2opabovd  7491  el2mpt2csbcl  7492  fnmpt2ovd  7494  fnmpt2ovdOLD  7495  ruclem1  15199  vdwapval  15913  vdwapid1  15915  vdwmc2  15919  vdwpc  15920  vdwlem5  15925  vdwlem8  15928  vdwlem13  15933  prdsval  16339  prdsdsval2  16368  pwsplusgval  16374  pwsmulrval  16375  pwsvscafval  16378  imasval  16395  iscat  16556  iscatd  16557  catidex  16558  catideu  16559  cidfval  16560  cidval  16561  catidd  16564  iscatd2  16565  catlid  16567  catrid  16568  homffval  16573  homfeqd  16578  homfeqval  16580  comfffval  16581  comffval  16582  comfeq  16589  comfeqd  16590  comfeqval  16591  catpropd  16592  oppcval  16596  oppcco  16600  monfval  16615  ismon  16616  oppcmon  16621  oppcepi  16622  sectffval  16633  sectfval  16634  invffval  16641  isoval  16648  dfiso2  16655  isofn  16658  invisoinvl  16673  invcoisoid  16675  isocoinvid  16676  issubc  16718  issubc3  16732  isfunc  16747  cofuval  16765  cofuval2  16770  funcres  16779  funcres2b  16780  funcres2  16781  funcres2c  16784  isfull  16793  isfth  16797  fullres2c  16822  natfval  16829  isnat  16830  fucval  16841  fucco  16845  fucpropd  16860  initoval  16870  termoval  16871  homarcl  16901  coafval  16937  resssetc  16965  resscatc  16978  catciso  16980  xpcval  17041  1stfval  17055  2ndfval  17058  prfval  17063  prfcl  17067  evlfval  17081  curfval  17087  curf1cl  17092  curfcl  17096  uncf1  17100  uncf2  17101  diag12  17108  diag2  17109  curf2ndf  17111  hofval  17116  hof1  17118  hof2fval  17119  hofcl  17123  yon12  17129  yon2  17130  hofpropd  17131  joinval  17229  meetval  17243  isdlat  17417  plusffval  17471  issstrmgm  17476  grpidval  17484  grpidd  17492  gsumvalx  17494  gsumpropd  17496  gsumress  17500  ismndd  17537  issubmnd  17542  submnd0  17544  ismhm  17561  issubm  17571  resmhm  17583  resmhm2  17584  resmhm2b  17585  isgrp  17652  isgrpd2e  17665  grpidd2  17683  grpinvfval  17684  imasgrp2  17754  imasgrp  17755  subg0  17821  subginv  17822  subgcl  17825  issubgrpd2  17831  isnsg  17844  isghm  17881  resghm  17897  isga  17944  subgga  17953  gasubg  17955  cntzfval  17973  resscntz  17984  odfval  18172  gexval  18213  lsmfval  18273  lsmvalx  18274  oppglsm  18277  subglsm  18306  pj1fval  18327  efgtval  18356  iscmn  18420  iscmnd  18425  submcmn2  18464  iscyg  18501  issrg  18728  isring  18772  ringidss  18798  prdsmgp  18831  mulgass3  18858  dvdsrval  18866  isirred  18920  isdrngd  18995  isdrngrd  18996  subrg1  19013  subrgmcl  19015  subrgdvds  19017  subrguss  19018  subrginv  19019  subrgdv  19020  subrgunit  19021  subrgugrp  19022  abvfval  19041  isabvd  19043  issrngd  19084  islmod  19090  islmodd  19092  scaffval  19104  lmodpropd  19149  lssset  19157  islssd  19159  prdslmodd  19195  islmhm  19253  reslmhm  19278  reslmhm2  19279  reslmhm2b  19280  islbs  19302  rlmvneg  19435  rrgval  19515  isassa  19543  isassad  19551  assamulgscmlem2  19577  psrval  19590  resspsradd  19644  resspsrmul  19645  resspsrvsca  19646  mplmon2mul  19728  ply1coe  19893  lply1binomsc  19904  evl1expd  19936  evl1scvarpw  19954  isphl  20202  ipffval  20222  isphld  20228  phssipval  20231  phssip  20232  phlssphl  20233  ocvfval  20240  isobs  20294  frlmplusgval  20337  frlmsubgval  20338  frlmvscafval  20339  frlmip  20347  frlmipval  20348  frlmup1  20367  lsslindf  20399  mamufval  20421  matplusg2  20463  matvsca2  20464  matplusgcell  20469  matsubgcell  20470  matinvgcell  20471  matvscacell  20472  matmulcell  20481  matmulcellOLD  20482  mpt2matmul  20483  mat1  20484  mattposm  20496  mat1dimmul  20513  dmatmul  20534  dmatcrng  20539  scmataddcl  20553  scmatsubcl  20554  scmatcrng  20558  smatvscl  20561  scmatghm  20570  scmatmhm  20571  mvmulfval  20579  ma1repveval  20608  mdetrlin  20639  mdetrsca  20640  mdetmul  20660  madurid  20681  minmar1cl  20689  smadiadetglem1  20709  smadiadetr  20713  matinv  20715  slesolinv  20718  slesolinvbi  20719  cramerimplem3  20724  cpmatacl  20754  mat2pmatghm  20768  decpmatmullem  20809  decpmatmul  20810  pmatcollpw1lem1  20812  pmatcollpw2lem  20815  pmatcollpwlem  20818  pmatcollpw3lem  20821  mply1topmatval  20842  mp2pm2mplem1  20844  mp2pm2mplem4  20847  mp2pm2mplem5  20848  mp2pm2mp  20849  chpmat1d  20874  chpscmatgsummon  20883  chfacfpmmulgsum2  20903  xkocnv  21851  submtmd  22141  prdsdsf  22405  ressprdsds  22409  blfvalps  22421  prdsxmslem2  22567  tmsxpsval  22576  ngpds  22641  sgrimval  22669  subgngp  22672  tngngp  22691  tngngp3  22693  isnlm  22712  lssnlm  22738  isphtpy  23013  isphtpc  23026  pi1cpbl  23076  pi1addf  23079  pi1addval  23080  pi1grplem  23081  clmsub  23112  clmvsass  23121  clmvsdir  23123  isclmp  23129  cvsi  23162  cvsdiv  23164  iscph  23202  cphdir  23237  cphdi  23238  cph2di  23239  cph2subdi  23242  cphass  23243  tchval  23249  ipcau2  23265  tchcphlem1  23266  tchcphlem2  23267  cphsscph  23282  caufval  23306  rrxip  23412  dvlip2  23994  q1pval  24149  r1pval  24152  dvntaylp  24361  efabl  24533  efsubm  24534  dchrmul  25209  istrkgc  25589  istrkgb  25590  istrkgcb  25591  istrkge  25592  istrkgl  25593  istrkgld  25594  iscgrg  25643  isismt  25665  tglngval  25682  legval  25715  ishlg  25733  mirval  25786  israg  25828  ishpg  25887  lmif  25913  islmib  25915  isinag  25965  ttgval  25991  wksonproplem  26851  wspthsnon  26996  iswwlksnon  26997  iswwlksnonOLD  26998  iswspthsnon  27001  iswspthsnonOLD  27002  isconngr  27384  isconngr1  27385  grpodivval  27740  dipfval  27907  ipval  27908  sspgval  27934  sspsval  27936  lnoval  27957  ajfval  28014  dipdir  28047  dipass  28050  htth  28125  isomnd  30048  submomnd  30057  inftmrel  30081  isinftm  30082  isslmd  30102  rngurd  30135  rdivmuldivd  30138  isorng  30146  suborng  30162  resv1r  30184  smatlem  30210  submatminr1  30223  metidval  30280  pstmval  30285  pstmfval  30286  zlm0  30353  zlm1  30354  sitmval  30758  breprexp  31058  istrkg2d  31091  afsval  31096  mclsrcl  31802  mppsval  31813  frecseq123  32119  matunitlindflem2  33737  istotbnd  33897  isbnd  33908  rrnequiv  33963  isrngo  34025  rngohomval  34092  idlval  34141  pridlval  34161  lflset  34857  islfld  34860  ldualvadd  34927  ldualsmul  34933  ldualvs  34935  isopos  34978  cmtfvalN  35008  iscvlat  35121  ishlat1  35150  lineset  35536  psubspset  35542  paddfval  35595  paddval  35596  ltrnfset  35915  trnfsetN  35953  trlfset  35958  tgrpov  36546  erngplus  36601  erngmul  36604  erngplus-rN  36609  erngmul-rN  36612  erngdvlem3  36788  erngdvlem4  36789  erng0g  36792  erngdvlem3-rN  36796  erngdvlem4-rN  36797  dvaplusg  36807  dvamulr  36810  dvavadd  36813  dvavsca  36815  dvalveclem  36823  dvhmulr  36884  dvhfvadd  36889  dvhvadd  36890  dvhopvadd2  36892  dvhvaddcl  36893  dvhvaddcomN  36894  dvhvsca  36899  dvhlveclem  36906  dvh0g  36909  djavalN  36933  diblsmopel  36969  dicvaddcl  36988  cdlemn6  37000  dihffval  37028  dihopelvalcpre  37046  djhval  37196  lcdvaddval  37396  lcdsmul  37400  lcdvsval  37402  lcdlkreq2N  37421  hvmapffval  37556  hvmapfval  37557  hdmap1fval  37594  hgmapffval  37683  hgmapfval  37684  hgmapadd  37692  hlhilipval  37747  hlhilhillem  37758  ioorrnopnlem  41020  hoidmvval0b  41303  hoidmvlelem2  41309  hoidmvlelem3  41310  hoidmvle  41313  ovnhoi  41316  hoiqssbl  41338  hspmbllem2  41340  vonioo  41395  vonicc  41398  ismgmd  42361  ismgmhm  42368  issubmgm  42374  resmgmhm  42383  resmgmhm2  42384  resmgmhm2b  42385  idfusubc  42451  rnghmval  42476  lidlmsgrp  42511  lidlrng  42512  zlidlring  42513  uzlidlring  42514  rnghmresel  42549  rngchom  42552  rngcco  42556  rnghmsubcsetclem1  42560  rhmresel  42595  ringchom  42598  ringcco  42602  rhmsubcsetclem1  42606  rhmsubcrngclem1  42612  irinitoringc  42654  ovmpt2rdxf  42702  lincop  42782  lincval  42783  lincsum  42803  lincscm  42804  lmod1lem2  42862  lmod1lem3  42863  lmod1lem4  42864  ldepsnlinc  42882
  Copyright terms: Public domain W3C validator