Theorem oveq 7366

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

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4587  ‘cfv 6493  (class class class)co 7360

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-ss 3919  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  oveqi  7373  oveqd  7377  ifov  7461  ovmpodf  7516  ovmpodv2  7518  seqomeq12  8387  mapxpen  9075  seqeq2  13932  relexp0g  14949  relexpsucnnr  14952  cat1  18025  ismgm  18570  mgmsscl  18574  issgrp  18649  ismnddef  18665  grpissubg  19080  isga  19224  isrng  20093  islmod  20819  lmodfopne  20855  mamuval  22341  dmatel  22441  dmatmulcl  22448  scmate  22458  scmateALT  22460  mvmulval  22491  marrepval0  22509  marepvval0  22514  submaval0  22528  mdetleib  22535  mdetleib1  22539  mdet0pr  22540  mdetunilem1  22560  maduval  22586  minmar1val0  22595  cpmatel  22659  mat2pmatval  22672  cpm2mval  22698  decpmatval0  22712  pmatcollpw3lem  22731  mptcoe1matfsupp  22750  mp2pm2mplem4  22757  chpscmat  22790  ispsmet  24252  ismet  24271  isxmet  24272  ishtpy  24931  isphtpy  24940  addsval  27962  mulsval  28109  isgrpo  30576  gidval  30591  grpoinvfval  30601  isablo  30625  vciOLD  30640  isvclem  30656  isnvlem  30689  isphg  30896  fxpval  33249  ofceq  34256  cvmlift2lem13  35511  ismtyval  38003  isass  38049  isexid  38050  elghomlem1OLD  38088  iscom2  38198  iscllaw  48502  iscomlaw  48503  isasslaw  48505  dmatALTbasel  48715  infsubc2  49373  nelsubc3lem  49382  dfswapf2  49573  isthinc  49731  cnelsubclem  49915  lanrcl  49933  ranrcl  49934  rellan  49935  relran  49936