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  27876  mulsval  28019  isgrpo  30445  gidval  30460  grpoinvfval  30470  isablo  30494  vciOLD  30509  isvclem  30525  isnvlem  30558  isphg  30765  fxpval  33116  ofceq  34080  cvmlift2lem13  35308  ismtyval  37800  isass  37846  isexid  37847  elghomlem1OLD  37885  iscom2  37995  iscllaw  48193  iscomlaw  48194  isasslaw  48196  dmatALTbasel  48407  infsubc2  49066  nelsubc3lem  49075  dfswapf2  49266  isthinc  49424  cnelsubclem  49608  lanrcl  49626  ranrcl  49627  rellan  49628  relran  49629