Theorem oveq 7156

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

Syntax hints:   → wi 4   = wceq 1533  ⟨cop 4566  ‘cfv 6349  (class class class)co 7150

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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rex 3144  df-uni 4832  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7153

This theorem is referenced by:  oveqi  7163  oveqd  7167  ifov  7248  ovmpodf  7300  ovmpodv2  7302  seqomeq12  8084  mapxpen  8677  seqeq2  13367  relexp0g  14375  relexpsucnnr  14378  ismgm  17847  mgmsscl  17851  issgrp  17896  ismnddef  17907  grpissubg  18293  isga  18415  islmod  19632  lmodfopne  19666  mamuval  20991  dmatel  21096  dmatmulcl  21103  scmate  21113  scmateALT  21115  mvmulval  21146  marrepval0  21164  marepvval0  21169  submaval0  21183  mdetleib  21190  mdetleib1  21194  mdet0pr  21195  mdetunilem1  21215  maduval  21241  minmar1val0  21250  cpmatel  21313  mat2pmatval  21326  cpm2mval  21352  decpmatval0  21366  pmatcollpw3lem  21385  mptcoe1matfsupp  21404  mp2pm2mplem4  21411  chpscmat  21444  ispsmet  22908  ismet  22927  isxmet  22928  ishtpy  23570  isphtpy  23579  isgrpo  28268  gidval  28283  grpoinvfval  28293  isablo  28317  vciOLD  28332  isvclem  28348  isnvlem  28381  isphg  28588  ofceq  31351  cvmlift2lem13  32557  ismtyval  35072  isass  35118  isexid  35119  elghomlem1OLD  35157  iscom2  35267  iscllaw  44090  iscomlaw  44091  isasslaw  44093  isrng  44141  dmatALTbasel  44451