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

Theorem oveqd 6544
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 6533 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  (class class class)co 6527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4368  df-br 4579  df-iota 5754  df-fv 5798  df-ov 6530
This theorem is referenced by:  oveq123d  6548  oveqdr  6551  csbov  6564  csbov12g  6565  ovmpt2dxf  6662  oprssov  6679  2mpt20  6758  ofeq  6775  el2mpt2csbcl  7115  fnmpt2ovd  7117  ruclem1  14748  vdwapval  15464  vdwapid1  15466  vdwmc2  15470  vdwpc  15471  vdwlem5  15476  vdwlem8  15479  vdwlem13  15484  prdsval  15887  prdsdsval2  15916  pwsplusgval  15922  pwsmulrval  15923  pwsvscafval  15926  imasval  15943  iscat  16105  iscatd  16106  catidex  16107  catideu  16108  cidfval  16109  cidval  16110  catidd  16113  iscatd2  16114  catlid  16116  catrid  16117  homffval  16122  homfeqd  16127  homfeqval  16129  comfffval  16130  comffval  16131  comfeq  16138  comfeqd  16139  comfeqval  16140  catpropd  16141  oppcval  16145  oppcco  16149  monfval  16164  ismon  16165  oppcmon  16170  oppcepi  16171  sectffval  16182  sectfval  16183  invffval  16190  isoval  16197  dfiso2  16204  isofn  16207  invisoinvl  16222  invcoisoid  16224  isocoinvid  16225  issubc  16267  issubc3  16281  isfunc  16296  cofuval  16314  cofuval2  16319  funcres  16328  funcres2b  16329  funcres2  16330  funcres2c  16333  isfull  16342  isfth  16346  fullres2c  16371  natfval  16378  isnat  16379  fucval  16390  fucco  16394  fucpropd  16409  initoval  16419  termoval  16420  homarcl  16450  coafval  16486  resssetc  16514  resscatc  16527  catciso  16529  xpcval  16589  1stfval  16603  2ndfval  16606  prfval  16611  prfcl  16615  evlfval  16629  curfval  16635  curf1cl  16640  curfcl  16644  uncf1  16648  uncf2  16649  diag12  16656  diag2  16657  curf2ndf  16659  hofval  16664  hof1  16666  hof2fval  16667  hofcl  16671  yon12  16677  yon2  16678  hofpropd  16679  joinval  16777  meetval  16791  isdlat  16965  plusffval  17019  issstrmgm  17024  grpidval  17032  grpidd  17040  gsumvalx  17042  gsumpropd  17044  gsumress  17048  ismndd  17085  issubmnd  17090  submnd0  17092  ismhm  17109  issubm  17119  resmhm  17131  resmhm2  17132  resmhm2b  17133  isgrp  17200  isgrpd2e  17213  grpidd2  17231  grpinvfval  17232  imasgrp2  17302  imasgrp  17303  subg0  17372  subginv  17373  subgcl  17376  issubgrpd2  17382  isnsg  17395  isghm  17432  resghm  17448  isga  17496  subgga  17505  gasubg  17507  cntzfval  17525  resscntz  17536  odfval  17724  gexval  17765  lsmfval  17825  lsmvalx  17826  oppglsm  17829  subglsm  17858  pj1fval  17879  efgtval  17908  iscmn  17972  iscmnd  17977  submcmn2  18016  iscyg  18053  issrg  18279  isring  18323  ringidss  18349  prdsmgp  18382  mulgass3  18409  dvdsrval  18417  isirred  18471  isdrngd  18544  isdrngrd  18545  subrg1  18562  subrgmcl  18564  subrgdvds  18566  subrguss  18567  subrginv  18568  subrgdv  18569  subrgunit  18570  subrgugrp  18571  abvfval  18590  isabvd  18592  issrngd  18633  islmod  18639  islmodd  18641  scaffval  18653  lmodpropd  18698  lssset  18704  islssd  18706  prdslmodd  18739  islmhm  18797  reslmhm  18822  reslmhm2  18823  reslmhm2b  18824  islbs  18846  rlmvneg  18977  rrgval  19057  isassa  19085  isassad  19093  assamulgscmlem2  19119  psrval  19132  resspsradd  19186  resspsrmul  19187  resspsrvsca  19188  mplmon2mul  19271  ply1coe  19436  lply1binomsc  19447  evl1expd  19479  evl1scvarpw  19497  isphl  19740  ipffval  19760  isphld  19766  phssipval  19769  phssip  19770  ocvfval  19777  isobs  19831  frlmplusgval  19874  frlmsubgval  19875  frlmvscafval  19876  frlmip  19884  frlmipval  19885  frlmup1  19904  lsslindf  19936  mamufval  19958  matplusg2  20000  matvsca2  20001  matplusgcell  20006  matsubgcell  20007  matinvgcell  20008  matvscacell  20009  matmulcell  20018  mpt2matmul  20019  mat1  20020  mattposm  20032  mat1dimmul  20049  dmatmul  20070  dmatcrng  20075  scmataddcl  20089  scmatsubcl  20090  scmatcrng  20094  smatvscl  20097  scmatghm  20106  scmatmhm  20107  mvmulfval  20115  ma1repveval  20144  mdetrlin  20175  mdetrsca  20176  mdetmul  20196  madurid  20217  minmar1cl  20224  smadiadetglem1  20244  smadiadetr  20248  matinv  20250  slesolinv  20253  slesolinvbi  20254  cramerimplem3  20258  cpmatacl  20288  mat2pmatghm  20302  decpmatmullem  20343  decpmatmul  20344  pmatcollpw1lem1  20346  pmatcollpw2lem  20349  pmatcollpwlem  20352  pmatcollpw3lem  20355  mply1topmatval  20376  mp2pm2mplem1  20378  mp2pm2mplem4  20381  mp2pm2mplem5  20382  mp2pm2mp  20383  chpmat1d  20408  chpscmatgsummon  20417  chfacfpmmulgsum2  20437  xkocnv  21375  submtmd  21666  prdsdsf  21930  ressprdsds  21934  blfvalps  21946  prdsxmslem2  22092  tmsxpsval  22101  ngpds  22166  sgrimval  22194  subgngp  22197  tngngp  22216  tngngp3  22218  isnlm  22237  lssnlm  22263  isphtpy  22536  isphtpc  22549  pi1cpbl  22600  pi1addf  22603  pi1addval  22604  pi1grplem  22605  clmsub  22636  clmvsass  22645  clmvsdir  22647  isclmp  22653  cvsi  22686  cvsdiv  22688  iscph  22723  cphdir  22758  cphdi  22759  cph2di  22760  cph2subdi  22763  cphass  22764  tchval  22770  ipcau2  22786  tchcphlem1  22787  tchcphlem2  22788  caufval  22826  rrxip  22931  dvlip2  23507  q1pval  23662  r1pval  23665  dvntaylp  23874  efabl  24045  efsubm  24046  dchrmul  24718  istrkgc  25098  istrkgb  25099  istrkgcb  25100  istrkge  25101  istrkgl  25102  istrkgld  25103  iscgrg  25153  isismt  25175  tglngval  25192  legval  25225  ishlg  25243  mirval  25296  israg  25338  ishpg  25397  lmif  25423  islmib  25425  isinag  25475  ttgval  25501  wlkon  25855  trlon  25864  trlonprop  25866  pthon  25899  pthonprop  25901  spthon  25906  spthonprp  25909  isconngra  25994  isconngra1  25995  is2wlkonot  26184  is2spthonot  26185  2wlkonot  26186  2spthonot  26187  2wlksot  26188  2spthsot  26189  2wlkonot3v  26196  2spthonot3v  26197  grpodivval  26567  dipfval  26735  ipval  26736  sspgval  26762  sspsval  26764  lnoval  26785  ajfval  26842  dipdir  26875  dipass  26878  htth  26953  isomnd  28826  submomnd  28835  inftmrel  28859  isinftm  28860  isslmd  28880  rngurd  28913  rdivmuldivd  28916  isorng  28924  suborng  28940  resv1r  28962  smatlem  28985  submatminr1  28998  metidval  29055  pstmval  29060  pstmfval  29061  zlm0  29128  zlm1  29129  sitmval  29532  istrkg2d  29791  afsval  29796  mclsrcl  30506  mppsval  30517  matunitlindflem2  32370  istotbnd  32532  isbnd  32543  rrnequiv  32598  isrngo  32660  rngohomval  32727  idlval  32776  pridlval  32796  lflset  33158  islfld  33161  ldualvadd  33228  ldualsmul  33234  ldualvs  33236  isopos  33279  cmtfvalN  33309  iscvlat  33422  ishlat1  33451  lineset  33836  psubspset  33842  paddfval  33895  paddval  33896  ltrnfset  34215  trnfsetN  34254  trlfset  34259  tgrpov  34848  erngplus  34903  erngmul  34906  erngplus-rN  34911  erngmul-rN  34914  erngdvlem3  35090  erngdvlem4  35091  erng0g  35094  erngdvlem3-rN  35098  erngdvlem4-rN  35099  dvaplusg  35109  dvamulr  35112  dvavadd  35115  dvavsca  35117  dvalveclem  35126  dvhmulr  35187  dvhfvadd  35192  dvhvadd  35193  dvhopvadd2  35195  dvhvaddcl  35196  dvhvaddcomN  35197  dvhvsca  35202  dvhlveclem  35209  dvh0g  35212  djavalN  35236  diblsmopel  35272  dicvaddcl  35291  cdlemn6  35303  dihffval  35331  dihopelvalcpre  35349  djhval  35499  lcdvaddval  35699  lcdsmul  35703  lcdvsval  35705  lcdlkreq2N  35724  hvmapffval  35859  hvmapfval  35860  hdmap1fval  35898  hgmapffval  35989  hgmapfval  35990  hgmapadd  35998  hlhilipval  36053  hlhilhillem  36064  ioorrnopnlem  38994  hoidmvval0b  39274  hoidmvlelem2  39280  hoidmvlelem3  39281  hoidmvle  39284  ovnhoi  39287  hoiqssbl  39309  hspmbllem2  39311  vonioo  39367  vonicc  39370  mptmpt2opabbrd  40152  mptmpt2opabovd  40153  1wlksonproplem  40904  wspthsnon  41042  iswwlksnon  41043  iswspthsnon  41044  wwlks2onv  41150  isconngr  41348  isconngr1  41349  ismgmd  41558  ismgmhm  41565  issubmgm  41571  resmgmhm  41580  resmgmhm2  41581  resmgmhm2b  41582  idfusubc  41648  rnghmval  41673  lidlmsgrp  41708  lidlrng  41709  zlidlring  41710  uzlidlring  41711  rnghmresel  41748  rngchom  41751  rngcco  41755  rnghmsubcsetclem1  41759  rhmresel  41794  ringchom  41797  ringcco  41801  rhmsubcsetclem1  41805  rhmsubcrngclem1  41811  irinitoringc  41853  ovmpt2rdxf  41902  lincop  41983  lincval  41984  lincsum  42004  lincscm  42005  lmod1lem2  42063  lmod1lem3  42064  lmod1lem4  42065  ldepsnlinc  42083
  Copyright terms: Public domain W3C validator