MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveq Structured version   Unicode version

Theorem oveq 6102
Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
oveq  |-  ( F  =  G  ->  ( A F B )  =  ( A G B ) )

Proof of Theorem oveq
StepHypRef Expression
1 fveq1 5695 . 2  |-  ( F  =  G  ->  ( F `  <. A ,  B >. )  =  ( G `  <. A ,  B >. ) )
2 df-ov 6099 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
3 df-ov 6099 . 2  |-  ( A G B )  =  ( G `  <. A ,  B >. )
41, 2, 33eqtr4g 2500 1  |-  ( F  =  G  ->  ( A F B )  =  ( A G B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   <.cop 3888   ` cfv 5423  (class class class)co 6096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rex 2726  df-uni 4097  df-br 4298  df-iota 5386  df-fv 5431  df-ov 6099
This theorem is referenced by:  oveqi  6109  oveqd  6113  ovmpt2df  6227  ovmpt2dv2  6229  seqomeq12  6914  mapxpen  7482  seqeq2  11815  grpissubg  15706  isga  15814  islmod  16957  mamuval  18289  mvmulval  18359  marrepval0  18377  marepvval0  18382  submaval0  18396  mdetleib  18403  mdetleib1  18407  mdet0pr  18408  mdetunilem1  18423  maduval  18449  minmar1val0  18458  ispsmet  19885  ismet  19903  isxmet  19904  ishtpy  20549  isphtpy  20558  isgrpo  23688  gidval  23705  grpoinvfval  23716  isablo  23775  isass  23808  isexid  23809  elghomlem1  23853  iscom2  23904  vci  23931  isvclem  23960  isnvlem  23993  isphg  24222  ofceq  26544  cvmlift2lem13  27209  relexp0  27336  relexpsucr  27337  ismtyval  28704  dmatid  30879  dmatelnd  30880  dmatsubcl  30882  dmatmulcl  30884  scmatid  30887  scmatsubcl  30889  scmatmulcl  30891  mptcoe1matfsupp  30896  pmatcollpw1lem1  30901  pmatcollpw1dst  30906  pmattomply1ghmlem2  30914  pmattomply1f1lem  30915  pmattomply1rn  30917  pmattomply1coe1  30919  idpmattoidmply1  30920  mp2pm2mplem3  30923  mp2pm2mplem4  30924  mp2pm2mplem5  30925  mp2pm2mp  30926  pmattomply1fo  30928  pmattomply1ghm  30930  pmattomply1mhmlem2  30934
  Copyright terms: Public domain W3C validator