Theorem oveq 7417

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

Syntax hints:   → wi 4   = wceq 1567  ⟨cop 4598  ‘cfv 6537  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-ss 3928  df-uni 4875  df-br 5112  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  oveqi  7424  oveqd  7428  ifov  7512  ovmpodf  7567  ovmpodv2  7569  seqomeq12  8441  mapxpen  9131  seqeq2  14041  relexp0g  15059  relexpsucnnr  15062  cat1  18154  ismgm  18699  mgmsscl  18703  issgrp  18778  ismnddef  18794  grpissubg  19213  isga  19361  isrng  20232  islmod  20963  lmodfopne  20999  mamuval  22519  dmatel  22619  dmatmulcl  22626  scmate  22636  scmateALT  22638  mvmulval  22669  marrepval0  22687  marepvval0  22692  submaval0  22706  mdetleib  22713  mdetleib1  22717  mdet0pr  22718  mdetunilem1  22738  maduval  22764  minmar1val0  22773  cpmatel  22837  mat2pmatval  22850  cpm2mval  22876  decpmatval0  22890  pmatcollpw3lem  22909  mptcoe1matfsupp  22928  mp2pm2mplem4  22935  chpscmat  22968  ispsmet  24430  ismet  24449  isxmet  24450  ishtpy  25100  isphtpy  25109  addsval  28121  mulsval  28268  isgrpo  30790  gidval  30805  grpoinvfval  30815  isablo  30839  vciOLD  30854  isvclem  30870  isnvlem  30903  isphg  31110  fxpval  33426  ofceq  34432  cvmlift2lem13  35740  nmulprop  36615  ismtyval  38374  isass  38420  isexid  38421  elghomlem1OLD  38459  iscom2  38569  iscllaw  48878  iscomlaw  48879  isasslaw  48881  dmatALTbasel  49102  infsubc2  49759  nelsubc3lem  49768  dfswapf2  49959  isthinc  50117  cnelsubclem  50301  lanrcl  50319  ranrcl  50320  rellan  50321  relran  50322