Theorem oveq 7352

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

Syntax hints:   → wi 4   = wceq 1541  ⟨cop 4579  ‘cfv 6481  (class class class)co 7346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  oveqi  7359  oveqd  7363  ifov  7447  ovmpodf  7502  ovmpodv2  7504  seqomeq12  8373  mapxpen  9056  seqeq2  13912  relexp0g  14929  relexpsucnnr  14932  cat1  18004  ismgm  18549  mgmsscl  18553  issgrp  18628  ismnddef  18644  grpissubg  19059  isga  19203  isrng  20072  islmod  20797  lmodfopne  20833  mamuval  22308  dmatel  22408  dmatmulcl  22415  scmate  22425  scmateALT  22427  mvmulval  22458  marrepval0  22476  marepvval0  22481  submaval0  22495  mdetleib  22502  mdetleib1  22506  mdet0pr  22507  mdetunilem1  22527  maduval  22553  minmar1val0  22562  cpmatel  22626  mat2pmatval  22639  cpm2mval  22665  decpmatval0  22679  pmatcollpw3lem  22698  mptcoe1matfsupp  22717  mp2pm2mplem4  22724  chpscmat  22757  ispsmet  24219  ismet  24238  isxmet  24239  ishtpy  24898  isphtpy  24907  addsval  27905  mulsval  28048  isgrpo  30477  gidval  30492  grpoinvfval  30502  isablo  30526  vciOLD  30541  isvclem  30557  isnvlem  30590  isphg  30797  fxpval  33134  ofceq  34110  cvmlift2lem13  35359  ismtyval  37839  isass  37885  isexid  37886  elghomlem1OLD  37924  iscom2  38034  iscllaw  48288  iscomlaw  48289  isasslaw  48291  dmatALTbasel  48502  infsubc2  49161  nelsubc3lem  49170  dfswapf2  49361  isthinc  49519  cnelsubclem  49703  lanrcl  49721  ranrcl  49722  rellan  49723  relran  49724