Theorem oveq 7219

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

Syntax hints:   → wi 4   = wceq 1543  ⟨cop 4547  ‘cfv 6380  (class class class)co 7213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-uni 4820  df-br 5054  df-iota 6338  df-fv 6388  df-ov 7216

This theorem is referenced by:  oveqi  7226  oveqd  7230  ifov  7311  ovmpodf  7365  ovmpodv2  7367  seqomeq12  8190  mapxpen  8812  seqeq2  13578  relexp0g  14585  relexpsucnnr  14588  cat1  17603  ismgm  18115  mgmsscl  18119  issgrp  18164  ismnddef  18175  grpissubg  18563  isga  18685  islmod  19903  lmodfopne  19937  mamuval  21285  dmatel  21390  dmatmulcl  21397  scmate  21407  scmateALT  21409  mvmulval  21440  marrepval0  21458  marepvval0  21463  submaval0  21477  mdetleib  21484  mdetleib1  21488  mdet0pr  21489  mdetunilem1  21509  maduval  21535  minmar1val0  21544  cpmatel  21608  mat2pmatval  21621  cpm2mval  21647  decpmatval0  21661  pmatcollpw3lem  21680  mptcoe1matfsupp  21699  mp2pm2mplem4  21706  chpscmat  21739  ispsmet  23202  ismet  23221  isxmet  23222  ishtpy  23869  isphtpy  23878  isgrpo  28578  gidval  28593  grpoinvfval  28603  isablo  28627  vciOLD  28642  isvclem  28658  isnvlem  28691  isphg  28898  ofceq  31777  cvmlift2lem13  32990  addsval  33863  ismtyval  35695  isass  35741  isexid  35742  elghomlem1OLD  35780  iscom2  35890  iscllaw  45056  iscomlaw  45057  isasslaw  45059  isrng  45107  dmatALTbasel  45416  isthinc  45975