Theorem oveq 7261

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 6755	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘⟨𝐴, 𝐵⟩) = (𝐺‘⟨𝐴, 𝐵⟩))
2		df-ov 7258	. 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3		df-ov 7258	. 2 ⊢ (𝐴𝐺𝐵) = (𝐺‘⟨𝐴, 𝐵⟩)
4	1, 2, 3	3eqtr4g 2804	1 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))

Syntax hints:   → wi 4   = wceq 1539  ⟨cop 4564  ‘cfv 6418  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  oveqi  7268  oveqd  7272  ifov  7353  ovmpodf  7407  ovmpodv2  7409  seqomeq12  8255  mapxpen  8879  seqeq2  13653  relexp0g  14661  relexpsucnnr  14664  cat1  17728  ismgm  18242  mgmsscl  18246  issgrp  18291  ismnddef  18302  grpissubg  18690  isga  18812  islmod  20042  lmodfopne  20076  mamuval  21445  dmatel  21550  dmatmulcl  21557  scmate  21567  scmateALT  21569  mvmulval  21600  marrepval0  21618  marepvval0  21623  submaval0  21637  mdetleib  21644  mdetleib1  21648  mdet0pr  21649  mdetunilem1  21669  maduval  21695  minmar1val0  21704  cpmatel  21768  mat2pmatval  21781  cpm2mval  21807  decpmatval0  21821  pmatcollpw3lem  21840  mptcoe1matfsupp  21859  mp2pm2mplem4  21866  chpscmat  21899  ispsmet  23365  ismet  23384  isxmet  23385  ishtpy  24041  isphtpy  24050  isgrpo  28760  gidval  28775  grpoinvfval  28785  isablo  28809  vciOLD  28824  isvclem  28840  isnvlem  28873  isphg  29080  ofceq  31965  cvmlift2lem13  33177  addsval  34053  ismtyval  35885  isass  35931  isexid  35932  elghomlem1OLD  35970  iscom2  36080  iscllaw  45271  iscomlaw  45272  isasslaw  45274  isrng  45322  dmatALTbasel  45631  isthinc  46190