Theorem oveq 7355

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4583  ‘cfv 6482  (class class class)co 7349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  oveqi  7362  oveqd  7366  ifov  7450  ovmpodf  7505  ovmpodv2  7507  seqomeq12  8376  mapxpen  9060  seqeq2  13912  relexp0g  14929  relexpsucnnr  14932  cat1  18004  ismgm  18515  mgmsscl  18519  issgrp  18594  ismnddef  18610  grpissubg  19025  isga  19170  isrng  20039  islmod  20767  lmodfopne  20803  mamuval  22278  dmatel  22378  dmatmulcl  22385  scmate  22395  scmateALT  22397  mvmulval  22428  marrepval0  22446  marepvval0  22451  submaval0  22465  mdetleib  22472  mdetleib1  22476  mdet0pr  22477  mdetunilem1  22497  maduval  22523  minmar1val0  22532  cpmatel  22596  mat2pmatval  22609  cpm2mval  22635  decpmatval0  22649  pmatcollpw3lem  22668  mptcoe1matfsupp  22687  mp2pm2mplem4  22694  chpscmat  22727  ispsmet  24190  ismet  24209  isxmet  24210  ishtpy  24869  isphtpy  24878  addsval  27874  mulsval  28017  isgrpo  30441  gidval  30456  grpoinvfval  30466  isablo  30490  vciOLD  30505  isvclem  30521  isnvlem  30554  isphg  30761  fxpval  33108  ofceq  34070  cvmlift2lem13  35298  ismtyval  37790  isass  37836  isexid  37837  elghomlem1OLD  37875  iscom2  37985  iscllaw  48183  iscomlaw  48184  isasslaw  48186  dmatALTbasel  48397  infsubc2  49056  nelsubc3lem  49065  dfswapf2  49256  isthinc  49414  cnelsubclem  49598  lanrcl  49616  ranrcl  49617  rellan  49618  relran  49619