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

Theorem oveq 6050
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 5690 . 2  |-  ( F  =  G  ->  ( F `  <. A ,  B >. )  =  ( G `  <. A ,  B >. ) )
2 df-ov 6047 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
3 df-ov 6047 . 2  |-  ( A G B )  =  ( G `  <. A ,  B >. )
41, 2, 33eqtr4g 2465 1  |-  ( F  =  G  ->  ( A F B )  =  ( A G B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   <.cop 3781   ` cfv 5417  (class class class)co 6044
This theorem is referenced by:  oveqi  6057  oveqd  6061  ovmpt2df  6168  ovmpt2dv2  6170  seqomeq12  6674  mapxpen  7236  seqeq2  11286  isga  15027  islmod  15913  ispsmet  18292  ismet  18310  isxmet  18311  ishtpy  18954  isphtpy  18963  isgrpo  21741  gidval  21758  grpoinvfval  21769  isablo  21828  isass  21861  isexid  21862  elghomlem1  21906  iscom2  21957  vci  21984  isvclem  22013  isnvlem  22046  isphg  22275  ofceq  24437  cvmlift2lem13  24959  relexp0  25086  relexpsucr  25087  ismtyval  26403  mamuval  27316  mdetleib  27360
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-rex 2676  df-uni 3980  df-br 4177  df-iota 5381  df-fv 5425  df-ov 6047
  Copyright terms: Public domain W3C validator