Theorem oveq 7373

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

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4573  ‘cfv 6498  (class class class)co 7367

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  oveqi  7380  oveqd  7384  ifov  7468  ovmpodf  7523  ovmpodv2  7525  seqomeq12  8393  mapxpen  9081  seqeq2  13967  relexp0g  14984  relexpsucnnr  14987  cat1  18064  ismgm  18609  mgmsscl  18613  issgrp  18688  ismnddef  18704  grpissubg  19122  isga  19266  isrng  20135  islmod  20859  lmodfopne  20895  mamuval  22358  dmatel  22458  dmatmulcl  22465  scmate  22475  scmateALT  22477  mvmulval  22508  marrepval0  22526  marepvval0  22531  submaval0  22545  mdetleib  22552  mdetleib1  22556  mdet0pr  22557  mdetunilem1  22577  maduval  22603  minmar1val0  22612  cpmatel  22676  mat2pmatval  22689  cpm2mval  22715  decpmatval0  22729  pmatcollpw3lem  22748  mptcoe1matfsupp  22767  mp2pm2mplem4  22774  chpscmat  22807  ispsmet  24269  ismet  24288  isxmet  24289  ishtpy  24939  isphtpy  24948  addsval  27954  mulsval  28101  isgrpo  30568  gidval  30583  grpoinvfval  30593  isablo  30617  vciOLD  30632  isvclem  30648  isnvlem  30681  isphg  30888  fxpval  33226  ofceq  34241  cvmlift2lem13  35497  ismtyval  38121  isass  38167  isexid  38168  elghomlem1OLD  38206  iscom2  38316  iscllaw  48665  iscomlaw  48666  isasslaw  48668  dmatALTbasel  48878  infsubc2  49536  nelsubc3lem  49545  dfswapf2  49736  isthinc  49894  cnelsubclem  50078  lanrcl  50096  ranrcl  50097  rellan  50098  relran  50099