Theorem oveq 7415

Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
oveq	⊢ (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))

Proof of Theorem oveq

Step	Hyp	Ref	Expression
1		fveq1 6891	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘⟨𝐴, 𝐵⟩) = (𝐺‘⟨𝐴, 𝐵⟩))
2		df-ov 7412	. 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3		df-ov 7412	. 2 ⊢ (𝐴𝐺𝐵) = (𝐺‘⟨𝐴, 𝐵⟩)
4	1, 2, 3	3eqtr4g 2798	1 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4635  ‘cfv 6544  (class class class)co 7409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  oveqi  7422  oveqd  7426  ifov  7509  ovmpodf  7564  ovmpodv2  7566  seqomeq12  8454  mapxpen  9143  seqeq2  13970  relexp0g  14969  relexpsucnnr  14972  cat1  18047  ismgm  18562  mgmsscl  18566  issgrp  18611  ismnddef  18627  grpissubg  19026  isga  19155  islmod  20475  lmodfopne  20510  mamuval  21888  dmatel  21995  dmatmulcl  22002  scmate  22012  scmateALT  22014  mvmulval  22045  marrepval0  22063  marepvval0  22068  submaval0  22082  mdetleib  22089  mdetleib1  22093  mdet0pr  22094  mdetunilem1  22114  maduval  22140  minmar1val0  22149  cpmatel  22213  mat2pmatval  22226  cpm2mval  22252  decpmatval0  22266  pmatcollpw3lem  22285  mptcoe1matfsupp  22304  mp2pm2mplem4  22311  chpscmat  22344  ispsmet  23810  ismet  23829  isxmet  23830  ishtpy  24488  isphtpy  24497  addsval  27446  mulsval  27565  isgrpo  29750  gidval  29765  grpoinvfval  29775  isablo  29799  vciOLD  29814  isvclem  29830  isnvlem  29863  isphg  30070  ofceq  33095  cvmlift2lem13  34306  ismtyval  36668  isass  36714  isexid  36715  elghomlem1OLD  36753  iscom2  36863  iscllaw  46599  iscomlaw  46600  isasslaw  46602  isrng  46650  dmatALTbasel  47083  isthinc  47641