Theorem oveq 7364

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

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4585  ‘cfv 6491  (class class class)co 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-uni 4863  df-br 5098  df-iota 6447  df-fv 6499  df-ov 7361

This theorem is referenced by:  oveqi  7371  oveqd  7375  ifov  7459  ovmpodf  7514  ovmpodv2  7516  seqomeq12  8385  mapxpen  9073  seqeq2  13930  relexp0g  14947  relexpsucnnr  14950  cat1  18023  ismgm  18568  mgmsscl  18572  issgrp  18647  ismnddef  18663  grpissubg  19078  isga  19222  isrng  20091  islmod  20817  lmodfopne  20853  mamuval  22339  dmatel  22439  dmatmulcl  22446  scmate  22456  scmateALT  22458  mvmulval  22489  marrepval0  22507  marepvval0  22512  submaval0  22526  mdetleib  22533  mdetleib1  22537  mdet0pr  22538  mdetunilem1  22558  maduval  22584  minmar1val0  22593  cpmatel  22657  mat2pmatval  22670  cpm2mval  22696  decpmatval0  22710  pmatcollpw3lem  22729  mptcoe1matfsupp  22748  mp2pm2mplem4  22755  chpscmat  22788  ispsmet  24250  ismet  24269  isxmet  24270  ishtpy  24929  isphtpy  24938  addsval  27942  mulsval  28089  isgrpo  30553  gidval  30568  grpoinvfval  30578  isablo  30602  vciOLD  30617  isvclem  30633  isnvlem  30666  isphg  30873  fxpval  33226  ofceq  34233  cvmlift2lem13  35488  ismtyval  37970  isass  38016  isexid  38017  elghomlem1OLD  38055  iscom2  38165  iscllaw  48472  iscomlaw  48473  isasslaw  48475  dmatALTbasel  48685  infsubc2  49343  nelsubc3lem  49352  dfswapf2  49543  isthinc  49701  cnelsubclem  49885  lanrcl  49903  ranrcl  49904  rellan  49905  relran  49906