Theorem oveq 7368

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

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4574  ‘cfv 6494  (class class class)co 7362

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 3432  df-ss 3907  df-uni 4852  df-br 5087  df-iota 6450  df-fv 6502  df-ov 7365

This theorem is referenced by:  oveqi  7375  oveqd  7379  ifov  7463  ovmpodf  7518  ovmpodv2  7520  seqomeq12  8388  mapxpen  9076  seqeq2  13962  relexp0g  14979  relexpsucnnr  14982  cat1  18059  ismgm  18604  mgmsscl  18608  issgrp  18683  ismnddef  18699  grpissubg  19117  isga  19261  isrng  20130  islmod  20854  lmodfopne  20890  mamuval  22372  dmatel  22472  dmatmulcl  22479  scmate  22489  scmateALT  22491  mvmulval  22522  marrepval0  22540  marepvval0  22545  submaval0  22559  mdetleib  22566  mdetleib1  22570  mdet0pr  22571  mdetunilem1  22591  maduval  22617  minmar1val0  22626  cpmatel  22690  mat2pmatval  22703  cpm2mval  22729  decpmatval0  22743  pmatcollpw3lem  22762  mptcoe1matfsupp  22781  mp2pm2mplem4  22788  chpscmat  22821  ispsmet  24283  ismet  24302  isxmet  24303  ishtpy  24953  isphtpy  24962  addsval  27972  mulsval  28119  isgrpo  30587  gidval  30602  grpoinvfval  30612  isablo  30636  vciOLD  30651  isvclem  30667  isnvlem  30700  isphg  30907  fxpval  33245  ofceq  34261  cvmlift2lem13  35517  ismtyval  38141  isass  38187  isexid  38188  elghomlem1OLD  38226  iscom2  38336  iscllaw  48683  iscomlaw  48684  isasslaw  48686  dmatALTbasel  48896  infsubc2  49554  nelsubc3lem  49563  dfswapf2  49754  isthinc  49912  cnelsubclem  50096  lanrcl  50114  ranrcl  50115  rellan  50116  relran  50117