Theorem oveq 7375

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4591  ‘cfv 6499  (class class class)co 7369

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 3446  df-ss 3928  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  oveqi  7382  oveqd  7386  ifov  7470  ovmpodf  7525  ovmpodv2  7527  seqomeq12  8399  mapxpen  9084  seqeq2  13946  relexp0g  14964  relexpsucnnr  14967  cat1  18039  ismgm  18550  mgmsscl  18554  issgrp  18629  ismnddef  18645  grpissubg  19060  isga  19205  isrng  20074  islmod  20802  lmodfopne  20838  mamuval  22313  dmatel  22413  dmatmulcl  22420  scmate  22430  scmateALT  22432  mvmulval  22463  marrepval0  22481  marepvval0  22486  submaval0  22500  mdetleib  22507  mdetleib1  22511  mdet0pr  22512  mdetunilem1  22532  maduval  22558  minmar1val0  22567  cpmatel  22631  mat2pmatval  22644  cpm2mval  22670  decpmatval0  22684  pmatcollpw3lem  22703  mptcoe1matfsupp  22722  mp2pm2mplem4  22729  chpscmat  22762  ispsmet  24225  ismet  24244  isxmet  24245  ishtpy  24904  isphtpy  24913  addsval  27909  mulsval  28052  isgrpo  30476  gidval  30491  grpoinvfval  30501  isablo  30525  vciOLD  30540  isvclem  30556  isnvlem  30589  isphg  30796  fxpval  33137  ofceq  34080  cvmlift2lem13  35295  ismtyval  37787  isass  37833  isexid  37834  elghomlem1OLD  37872  iscom2  37982  iscllaw  48170  iscomlaw  48171  isasslaw  48173  dmatALTbasel  48384  infsubc2  49043  nelsubc3lem  49052  dfswapf2  49243  isthinc  49401  cnelsubclem  49585  lanrcl  49603  ranrcl  49604  rellan  49605  relran  49606