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

Theorem oveq 5864
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 5524 . 2  |-  ( F  =  G  ->  ( F `  <. A ,  B >. )  =  ( G `  <. A ,  B >. ) )
2 df-ov 5861 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
3 df-ov 5861 . 2  |-  ( A G B )  =  ( G `  <. A ,  B >. )
41, 2, 33eqtr4g 2340 1  |-  ( F  =  G  ->  ( A F B )  =  ( A G B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   <.cop 3643   ` cfv 5255  (class class class)co 5858
This theorem is referenced by:  oveqi  5871  oveqd  5875  ovmpt2df  5979  ovmpt2dv2  5981  seqomeq12  6466  mapxpen  7027  seqeq2  11050  isga  14745  islmod  15631  ismet  17888  isxmet  17889  ishtpy  18470  isphtpy  18479  isgrpo  20863  gidval  20880  grpoinvfval  20891  isablo  20950  isass  20983  isexid  20984  elghomlem1  21028  iscom2  21079  vci  21104  isvclem  21133  isnvlem  21166  isphg  21395  ofceq  23458  cvmlift2lem13  23846  relexp0  24025  relexpsucr  24026  islatalg  25183  iscom  25333  com2i  25416  vecval1b  25451  vecval3b  25452  vri  25492  cnegvex2  25660  rnegvex2  25661  addcanrg  25667  issubcv  25670  isucv  25677  ismulcv  25681  isded  25736  dedi  25737  iscatOLD  25754  cati  25755  ismona  25809  isibg2  26110  isibcg  26191  ismtyval  26524  mamuval  27444  mdetleib  27488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator