Theorem oveq 7141

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

Syntax hints:   → wi 4   = wceq 1538  ⟨cop 4531  ‘cfv 6324  (class class class)co 7135

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  oveqi  7148  oveqd  7152  ifov  7233  ovmpodf  7285  ovmpodv2  7287  seqomeq12  8073  mapxpen  8667  seqeq2  13368  relexp0g  14373  relexpsucnnr  14376  ismgm  17845  mgmsscl  17849  issgrp  17894  ismnddef  17905  grpissubg  18291  isga  18413  islmod  19631  lmodfopne  19665  mamuval  20993  dmatel  21098  dmatmulcl  21105  scmate  21115  scmateALT  21117  mvmulval  21148  marrepval0  21166  marepvval0  21171  submaval0  21185  mdetleib  21192  mdetleib1  21196  mdet0pr  21197  mdetunilem1  21217  maduval  21243  minmar1val0  21252  cpmatel  21316  mat2pmatval  21329  cpm2mval  21355  decpmatval0  21369  pmatcollpw3lem  21388  mptcoe1matfsupp  21407  mp2pm2mplem4  21414  chpscmat  21447  ispsmet  22911  ismet  22930  isxmet  22931  ishtpy  23577  isphtpy  23586  isgrpo  28280  gidval  28295  grpoinvfval  28305  isablo  28329  vciOLD  28344  isvclem  28360  isnvlem  28393  isphg  28600  ofceq  31466  cvmlift2lem13  32675  ismtyval  35238  isass  35284  isexid  35285  elghomlem1OLD  35323  iscom2  35433  iscllaw  44449  iscomlaw  44450  isasslaw  44452  isrng  44500  dmatALTbasel  44811