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

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

Proof of Theorem oveq
StepHypRef Expression
1 fveq1 6654 . 2 (𝐹 = 𝐺 → (𝐹‘⟨𝐴, 𝐵⟩) = (𝐺‘⟨𝐴, 𝐵⟩))
2 df-ov 7148 . 2 (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3 df-ov 7148 . 2 (𝐴𝐺𝐵) = (𝐺‘⟨𝐴, 𝐵⟩)
41, 2, 33eqtr4g 2858 1 (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538  ⟨cop 4534  ‘cfv 6332  (class class class)co 7145 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3444  df-in 3890  df-ss 3900  df-uni 4805  df-br 5035  df-iota 6291  df-fv 6340  df-ov 7148 This theorem is referenced by:  oveqi  7158  oveqd  7162  ifov  7243  ovmpodf  7296  ovmpodv2  7298  seqomeq12  8091  mapxpen  8685  seqeq2  13388  relexp0g  14393  relexpsucnnr  14396  ismgm  17865  mgmsscl  17869  issgrp  17914  ismnddef  17925  grpissubg  18312  isga  18434  islmod  19652  lmodfopne  19686  mamuval  21034  dmatel  21139  dmatmulcl  21146  scmate  21156  scmateALT  21158  mvmulval  21189  marrepval0  21207  marepvval0  21212  submaval0  21226  mdetleib  21233  mdetleib1  21237  mdet0pr  21238  mdetunilem1  21258  maduval  21284  minmar1val0  21293  cpmatel  21357  mat2pmatval  21370  cpm2mval  21396  decpmatval0  21410  pmatcollpw3lem  21429  mptcoe1matfsupp  21448  mp2pm2mplem4  21455  chpscmat  21488  ispsmet  22952  ismet  22971  isxmet  22972  ishtpy  23618  isphtpy  23627  isgrpo  28324  gidval  28339  grpoinvfval  28349  isablo  28373  vciOLD  28388  isvclem  28404  isnvlem  28437  isphg  28644  ofceq  31532  cvmlift2lem13  32741  ismtyval  35389  isass  35435  isexid  35436  elghomlem1OLD  35474  iscom2  35584  iscllaw  44617  iscomlaw  44618  isasslaw  44620  isrng  44668  dmatALTbasel  44977
 Copyright terms: Public domain W3C validator