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

Theorem oveq 6302
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 5871 . 2  |-  ( F  =  G  ->  ( F `  <. A ,  B >. )  =  ( G `  <. A ,  B >. ) )
2 df-ov 6299 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
3 df-ov 6299 . 2  |-  ( A G B )  =  ( G `  <. A ,  B >. )
41, 2, 33eqtr4g 2486 1  |-  ( F  =  G  ->  ( A F B )  =  ( A G B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   <.cop 3999   ` cfv 5592  (class class class)co 6296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rex 2779  df-uni 4214  df-br 4418  df-iota 5556  df-fv 5600  df-ov 6299
This theorem is referenced by:  oveqi  6309  oveqd  6313  ifov  6381  ovmpt2df  6433  ovmpt2dv2  6435  seqomeq12  7170  mapxpen  7735  seqeq2  12203  relexp0g  13053  relexpsucnnr  13056  ismgm  16433  issgrp  16472  ismnddef  16482  grpissubg  16781  isga  16889  islmod  18023  mamuval  19335  dmatel  19442  dmatmulcl  19449  scmate  19459  scmateALT  19461  mvmulval  19492  marrepval0  19510  marepvval0  19515  submaval0  19529  mdetleib  19536  mdetleib1  19540  mdet0pr  19541  mdetunilem1  19561  maduval  19587  minmar1val0  19596  cpmatel  19659  mat2pmatval  19672  cpm2mval  19698  decpmatval0  19712  pmatcollpw3lem  19731  mptcoe1matfsupp  19750  mp2pm2mplem4  19757  chpscmat  19790  ispsmet  21244  ismet  21262  isxmet  21263  ishtpy  21909  isphtpy  21918  isgrpo  25795  gidval  25812  grpoinvfval  25823  isablo  25882  isass  25915  isexid  25916  elghomlem1OLD  25960  iscom2  26011  vci  26038  isvclem  26067  isnvlem  26100  isphg  26329  ofceq  28783  cvmlift2lem13  29852  ismtyval  31865  iscllaw  38625  iscomlaw  38626  isasslaw  38628  isrng  38676  dmatALTbasel  38997
  Copyright terms: Public domain W3C validator