Theorem oveq 7437

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

Syntax hints:   → wi 4   = wceq 1537  ⟨cop 4637  ‘cfv 6563  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434

This theorem is referenced by:  oveqi  7444  oveqd  7448  ifov  7534  ovmpodf  7589  ovmpodv2  7591  seqomeq12  8493  mapxpen  9182  seqeq2  14043  relexp0g  15058  relexpsucnnr  15061  cat1  18151  ismgm  18667  mgmsscl  18671  issgrp  18746  ismnddef  18762  grpissubg  19177  isga  19322  isrng  20172  islmod  20879  lmodfopne  20915  mamuval  22413  dmatel  22515  dmatmulcl  22522  scmate  22532  scmateALT  22534  mvmulval  22565  marrepval0  22583  marepvval0  22588  submaval0  22602  mdetleib  22609  mdetleib1  22613  mdet0pr  22614  mdetunilem1  22634  maduval  22660  minmar1val0  22669  cpmatel  22733  mat2pmatval  22746  cpm2mval  22772  decpmatval0  22786  pmatcollpw3lem  22805  mptcoe1matfsupp  22824  mp2pm2mplem4  22831  chpscmat  22864  ispsmet  24330  ismet  24349  isxmet  24350  ishtpy  25018  isphtpy  25027  addsval  28010  mulsval  28150  isgrpo  30526  gidval  30541  grpoinvfval  30551  isablo  30575  vciOLD  30590  isvclem  30606  isnvlem  30639  isphg  30846  ofceq  34078  cvmlift2lem13  35300  ismtyval  37787  isass  37833  isexid  37834  elghomlem1OLD  37872  iscom2  37982  iscllaw  48033  iscomlaw  48034  isasslaw  48036  dmatALTbasel  48248  isthinc  48821