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

Theorem oveq 5951
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 5607 . 2  |-  ( F  =  G  ->  ( F `  <. A ,  B >. )  =  ( G `  <. A ,  B >. ) )
2 df-ov 5948 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
3 df-ov 5948 . 2  |-  ( A G B )  =  ( G `  <. A ,  B >. )
41, 2, 33eqtr4g 2415 1  |-  ( F  =  G  ->  ( A F B )  =  ( A G B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642   <.cop 3719   ` cfv 5337  (class class class)co 5945
This theorem is referenced by:  oveqi  5958  oveqd  5962  ovmpt2df  6066  ovmpt2dv2  6068  seqomeq12  6553  mapxpen  7115  seqeq2  11142  isga  14844  islmod  15730  ismet  17990  isxmet  17991  ishtpy  18574  isphtpy  18583  isgrpo  20975  gidval  20992  grpoinvfval  21003  isablo  21062  isass  21095  isexid  21096  elghomlem1  21140  iscom2  21191  vci  21218  isvclem  21247  isnvlem  21280  isphg  21509  ofceq  23746  cvmlift2lem13  24250  relexp0  24429  relexpsucr  24430  ismtyval  25847  mamuval  26767  mdetleib  26811
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rex 2625  df-uni 3909  df-br 4105  df-iota 5301  df-fv 5345  df-ov 5948
  Copyright terms: Public domain W3C validator