Theorem oveq 7290

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

Syntax hints:   → wi 4   = wceq 1539  ⟨cop 4568  ‘cfv 6437  (class class class)co 7284

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  oveqi  7297  oveqd  7301  ifov  7384  ovmpodf  7438  ovmpodv2  7440  seqomeq12  8294  mapxpen  8939  seqeq2  13734  relexp0g  14742  relexpsucnnr  14745  cat1  17821  ismgm  18336  mgmsscl  18340  issgrp  18385  ismnddef  18396  grpissubg  18784  isga  18906  islmod  20136  lmodfopne  20170  mamuval  21544  dmatel  21651  dmatmulcl  21658  scmate  21668  scmateALT  21670  mvmulval  21701  marrepval0  21719  marepvval0  21724  submaval0  21738  mdetleib  21745  mdetleib1  21749  mdet0pr  21750  mdetunilem1  21770  maduval  21796  minmar1val0  21805  cpmatel  21869  mat2pmatval  21882  cpm2mval  21908  decpmatval0  21922  pmatcollpw3lem  21941  mptcoe1matfsupp  21960  mp2pm2mplem4  21967  chpscmat  22000  ispsmet  23466  ismet  23485  isxmet  23486  ishtpy  24144  isphtpy  24153  isgrpo  28868  gidval  28883  grpoinvfval  28893  isablo  28917  vciOLD  28932  isvclem  28948  isnvlem  28981  isphg  29188  ofceq  32074  cvmlift2lem13  33286  addsval  34135  ismtyval  35967  isass  36013  isexid  36014  elghomlem1OLD  36052  iscom2  36162  iscllaw  45394  iscomlaw  45395  isasslaw  45397  isrng  45445  dmatALTbasel  45754  isthinc  46313