Theorem oveq 7411

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

Syntax hints:   → wi 4   = wceq 1541  ⟨cop 4633  ‘cfv 6540  (class class class)co 7405

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408

This theorem is referenced by:  oveqi  7418  oveqd  7422  ifov  7505  ovmpodf  7560  ovmpodv2  7562  seqomeq12  8450  mapxpen  9139  seqeq2  13966  relexp0g  14965  relexpsucnnr  14968  cat1  18043  ismgm  18558  mgmsscl  18562  issgrp  18607  ismnddef  18623  grpissubg  19020  isga  19149  islmod  20467  lmodfopne  20502  mamuval  21879  dmatel  21986  dmatmulcl  21993  scmate  22003  scmateALT  22005  mvmulval  22036  marrepval0  22054  marepvval0  22059  submaval0  22073  mdetleib  22080  mdetleib1  22084  mdet0pr  22085  mdetunilem1  22105  maduval  22131  minmar1val0  22140  cpmatel  22204  mat2pmatval  22217  cpm2mval  22243  decpmatval0  22257  pmatcollpw3lem  22276  mptcoe1matfsupp  22295  mp2pm2mplem4  22302  chpscmat  22335  ispsmet  23801  ismet  23820  isxmet  23821  ishtpy  24479  isphtpy  24488  addsval  27435  mulsval  27554  isgrpo  29737  gidval  29752  grpoinvfval  29762  isablo  29786  vciOLD  29801  isvclem  29817  isnvlem  29850  isphg  30057  ofceq  33083  cvmlift2lem13  34294  ismtyval  36656  isass  36702  isexid  36703  elghomlem1OLD  36741  iscom2  36851  iscllaw  46585  iscomlaw  46586  isasslaw  46588  isrng  46636  dmatALTbasel  47036  isthinc  47594