Theorem oveq 7343

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4579  ‘cfv 6479  (class class class)co 7337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915  df-uni 4853  df-br 5093  df-iota 6431  df-fv 6487  df-ov 7340

This theorem is referenced by:  oveqi  7350  oveqd  7354  ifov  7437  ovmpodf  7491  ovmpodv2  7493  seqomeq12  8355  mapxpen  9008  seqeq2  13826  relexp0g  14832  relexpsucnnr  14835  cat1  17909  ismgm  18424  mgmsscl  18428  issgrp  18473  ismnddef  18484  grpissubg  18871  isga  18993  islmod  20233  lmodfopne  20267  mamuval  21641  dmatel  21748  dmatmulcl  21755  scmate  21765  scmateALT  21767  mvmulval  21798  marrepval0  21816  marepvval0  21821  submaval0  21835  mdetleib  21842  mdetleib1  21846  mdet0pr  21847  mdetunilem1  21867  maduval  21893  minmar1val0  21902  cpmatel  21966  mat2pmatval  21979  cpm2mval  22005  decpmatval0  22019  pmatcollpw3lem  22038  mptcoe1matfsupp  22057  mp2pm2mplem4  22064  chpscmat  22097  ispsmet  23563  ismet  23582  isxmet  23583  ishtpy  24241  isphtpy  24250  isgrpo  29147  gidval  29162  grpoinvfval  29172  isablo  29196  vciOLD  29211  isvclem  29227  isnvlem  29260  isphg  29467  ofceq  32363  cvmlift2lem13  33576  addsval  34222  ismtyval  36071  isass  36117  isexid  36118  elghomlem1OLD  36156  iscom2  36266  iscllaw  45742  iscomlaw  45743  isasslaw  45745  isrng  45793  dmatALTbasel  46102  isthinc  46661