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

Theorem oveq 6848
Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
oveq (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))

Proof of Theorem oveq
StepHypRef Expression
1 fveq1 6374 . 2 (𝐹 = 𝐺 → (𝐹‘⟨𝐴, 𝐵⟩) = (𝐺‘⟨𝐴, 𝐵⟩))
2 df-ov 6845 . 2 (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3 df-ov 6845 . 2 (𝐴𝐺𝐵) = (𝐺‘⟨𝐴, 𝐵⟩)
41, 2, 33eqtr4g 2824 1 (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  cop 4340  cfv 6068  (class class class)co 6842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rex 3061  df-uni 4595  df-br 4810  df-iota 6031  df-fv 6076  df-ov 6845
This theorem is referenced by:  oveqi  6855  oveqd  6859  ifov  6938  ovmpt2df  6990  ovmpt2dv2  6992  seqomeq12  7753  mapxpen  8333  seqeq2  13012  relexp0g  14049  relexpsucnnr  14052  ismgm  17511  issgrp  17553  ismnddef  17564  grpissubg  17880  isga  17989  islmod  19136  lmodfopne  19170  mamuval  20468  dmatel  20576  dmatmulcl  20583  scmate  20593  scmateALT  20595  mvmulval  20626  marrepval0  20644  marepvval0  20649  submaval0  20663  mdetleib  20670  mdetleib1  20674  mdet0pr  20675  mdetunilem1  20695  maduval  20721  minmar1val0  20730  cpmatel  20795  mat2pmatval  20808  cpm2mval  20834  decpmatval0  20848  pmatcollpw3lem  20867  mptcoe1matfsupp  20886  mp2pm2mplem4  20893  chpscmat  20926  ispsmet  22388  ismet  22407  isxmet  22408  ishtpy  23050  isphtpy  23059  isgrpo  27743  gidval  27758  grpoinvfval  27768  isablo  27792  vciOLD  27807  isvclem  27823  isnvlem  27856  isphg  28063  ofceq  30541  cvmlift2lem13  31677  ismtyval  33953  isass  33999  isexid  34000  elghomlem1OLD  34038  iscom2  34148  iscllaw  42426  iscomlaw  42427  isasslaw  42429  isrng  42477  dmatALTbasel  42792
  Copyright terms: Public domain W3C validator