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

Syntax hints:   → wi 4   = wceq 1548  ⟨cop 4564  ‘cfv 6489  (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 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-uni 4842  df-br 5076  df-iota 6445  df-fv 6497  df-ov 7363

This theorem is referenced by:  oveqi  7373  oveqd  7377  ifov  7461  ovmpodf  7516  ovmpodv2  7518  seqomeq12  8387  mapxpen  9075  seqeq2  13962  relexp0g  14979  relexpsucnnr  14982  cat1  18059  ismgm  18604  mgmsscl  18608  issgrp  18683  ismnddef  18699  grpissubg  19117  isga  19261  isrng  20130  islmod  20858  lmodfopne  20894  mamuval  22380  dmatel  22480  dmatmulcl  22487  scmate  22497  scmateALT  22499  mvmulval  22530  marrepval0  22548  marepvval0  22553  submaval0  22567  mdetleib  22574  mdetleib1  22578  mdet0pr  22579  mdetunilem1  22599  maduval  22625  minmar1val0  22634  cpmatel  22698  mat2pmatval  22711  cpm2mval  22737  decpmatval0  22751  pmatcollpw3lem  22770  mptcoe1matfsupp  22789  mp2pm2mplem4  22796  chpscmat  22829  ispsmet  24291  ismet  24310  isxmet  24311  ishtpy  24961  isphtpy  24970  addsval  27976  mulsval  28123  isgrpo  30590  gidval  30605  grpoinvfval  30615  isablo  30639  vciOLD  30654  isvclem  30670  isnvlem  30703  isphg  30910  fxpval  33250  ofceq  34293  cvmlift2lem13  35558  ismtyval  38182  isass  38228  isexid  38229  elghomlem1OLD  38267  iscom2  38377  iscllaw  48694  iscomlaw  48695  isasslaw  48697  dmatALTbasel  48907  infsubc2  49565  nelsubc3lem  49574  dfswapf2  49765  isthinc  49923  cnelsubclem  50107  lanrcl  50125  ranrcl  50126  rellan  50127  relran  50128