Theorem oveq 7446

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4838  ‘cfv 6555  (class class class)co 7440

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871  df-br 5107  df-iota 6509  df-fv 6563  df-ov 7443

This theorem is used by:  oveqi  7453  oveqd  7457  ifov  7541  ovmpodf  7597  ovmpodv2  7599  seqomeq12  8489  mapxpen  9187  seqeq2  14172  relexp0g  15201  relexpsucnnr  15204  cat1  18298  ismgm  18843  mgmsscl  18847  issgrp  18935  ismnddef  18951  grpissubg  19383  isga  19532  isrng  20403  islmod  21166  lmodfopne  21202  mamuval  22735  dmatel  22835  dmatmulcl  22842  scmate  22852  scmateALT  22854  mvmulval  22885  marrepval0  22903  marepvval0  22908  submaval0  22922  mdetleib  22929  mdetleib1  22933  mdet0pr  22934  mdetunilem1  22954  maduval  22980  minmar1val0  22989  cpmatel  23056  mat2pmatval  23069  cpm2mval  23095  decpmatval0  23109  pmatcollpw3lem  23128  mptcoe1matfsupp  23147  mp2pm2mplem4  23154  chpscmat  23187  ispsmet  24650  ismet  24669  isxmet  24670  ishtpy  25320  isphtpy  25329  addsval  28375  mulsval  28522  isgrpo  31126  gidval  31141  grpoinvfval  31151  isablo  31175  vciOLD  31190  isvclem  31206  isnvlem  31239  isphg  31446  fxpval  33793  ofceq  34796  cvmlift2lem13  36246  nmulprop  37116  ismtyval  38925  isass  38971  isexid  38972  elghomlem1OLD  39010  iscom2  39120  iscllaw  49489  iscomlaw  49490  isasslaw  49492  dmatALTbasel  49717  infsubc2  50378  nelsubc3lem  50387  dfswapf2  50586  isthinc  50757  cnelsubcw  50944  lanrcl  51007  ranrcl  51008  rellan  51009  relran  51010