Theorem oveq 7426

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ⟨cop 4589  ‘cfv 6538  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  oveqi  7433  oveqd  7437  ifov  7521  ovmpodf  7576  ovmpodv2  7578  seqomeq12  8464  mapxpen  9162  seqeq2  14148  relexp0g  15175  relexpsucnnr  15178  cat1  18272  ismgm  18817  mgmsscl  18821  issgrp  18909  ismnddef  18925  grpissubg  19357  isga  19505  isrng  20376  islmod  21139  lmodfopne  21175  mamuval  22708  dmatel  22808  dmatmulcl  22815  scmate  22825  scmateALT  22827  mvmulval  22858  marrepval0  22876  marepvval0  22881  submaval0  22895  mdetleib  22902  mdetleib1  22906  mdet0pr  22907  mdetunilem1  22927  maduval  22953  minmar1val0  22962  cpmatel  23029  mat2pmatval  23042  cpm2mval  23068  decpmatval0  23082  pmatcollpw3lem  23101  mptcoe1matfsupp  23120  mp2pm2mplem4  23127  chpscmat  23160  ispsmet  24623  ismet  24642  isxmet  24643  ishtpy  25293  isphtpy  25302  addsval  28348  mulsval  28495  isgrpo  31099  gidval  31114  grpoinvfval  31124  isablo  31148  vciOLD  31163  isvclem  31179  isnvlem  31212  isphg  31419  fxpval  33726  ofceq  34729  cvmlift2lem13  36080  nmulprop  36939  ismtyval  38735  isass  38781  isexid  38782  elghomlem1OLD  38820  iscom2  38930  iscllaw  49286  iscomlaw  49287  isasslaw  49289  dmatALTbasel  49514  infsubc2  50169  nelsubc3lem  50178  dfswapf2  50369  isthinc  50527  cnelsubclem  50711  lanrcl  50729  ranrcl  50730  rellan  50731  relran  50732