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

Theorem oveq 6290
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 5865 . 2  |-  ( F  =  G  ->  ( F `  <. A ,  B >. )  =  ( G `  <. A ,  B >. ) )
2 df-ov 6287 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
3 df-ov 6287 . 2  |-  ( A G B )  =  ( G `  <. A ,  B >. )
41, 2, 33eqtr4g 2533 1  |-  ( F  =  G  ->  ( A F B )  =  ( A G B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   <.cop 4033   ` cfv 5588  (class class class)co 6284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6287
This theorem is referenced by:  oveqi  6297  oveqd  6301  ifov  6366  ovmpt2df  6418  ovmpt2dv2  6420  seqomeq12  7119  mapxpen  7683  seqeq2  12079  grpissubg  16026  isga  16134  islmod  17316  mamuval  18683  dmatel  18790  dmatmulcl  18797  scmate  18807  scmateALT  18809  mvmulval  18840  marrepval0  18858  marepvval0  18863  submaval0  18877  mdetleib  18884  mdetleib1  18888  mdet0pr  18889  mdetunilem1  18909  maduval  18935  minmar1val0  18944  cpmatel  19007  mat2pmatval  19020  cpm2mval  19046  decpmatval0  19060  pmatcollpw3lem  19079  mptcoe1matfsupp  19098  mp2pm2mplem4  19105  chpscmat  19138  ispsmet  20571  ismet  20589  isxmet  20590  ishtpy  21235  isphtpy  21244  isgrpo  24902  gidval  24919  grpoinvfval  24930  isablo  24989  isass  25022  isexid  25023  elghomlem1  25067  iscom2  25118  vci  25145  isvclem  25174  isnvlem  25207  isphg  25436  ofceq  27764  cvmlift2lem13  28428  relexp0  28555  relexpsucr  28556  ismtyval  29927  ismgmALT  31951  issgrp  31954  iscllaw  31969  iscomlaw  31970  isasslaw  31972  isrng0  32013  dmatALTbasel  32102
  Copyright terms: Public domain W3C validator