Theorem oveq 7393

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4595  ‘cfv 6511  (class class class)co 7387

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 3449  df-ss 3931  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  oveqi  7400  oveqd  7404  ifov  7490  ovmpodf  7545  ovmpodv2  7547  seqomeq12  8422  mapxpen  9107  seqeq2  13970  relexp0g  14988  relexpsucnnr  14991  cat1  18059  ismgm  18568  mgmsscl  18572  issgrp  18647  ismnddef  18663  grpissubg  19078  isga  19223  isrng  20063  islmod  20770  lmodfopne  20806  mamuval  22280  dmatel  22380  dmatmulcl  22387  scmate  22397  scmateALT  22399  mvmulval  22430  marrepval0  22448  marepvval0  22453  submaval0  22467  mdetleib  22474  mdetleib1  22478  mdet0pr  22479  mdetunilem1  22499  maduval  22525  minmar1val0  22534  cpmatel  22598  mat2pmatval  22611  cpm2mval  22637  decpmatval0  22651  pmatcollpw3lem  22670  mptcoe1matfsupp  22689  mp2pm2mplem4  22696  chpscmat  22729  ispsmet  24192  ismet  24211  isxmet  24212  ishtpy  24871  isphtpy  24880  addsval  27869  mulsval  28012  isgrpo  30426  gidval  30441  grpoinvfval  30451  isablo  30475  vciOLD  30490  isvclem  30506  isnvlem  30539  isphg  30746  fxpval  33122  ofceq  34087  cvmlift2lem13  35302  ismtyval  37794  isass  37840  isexid  37841  elghomlem1OLD  37879  iscom2  37989  iscllaw  48177  iscomlaw  48178  isasslaw  48180  dmatALTbasel  48391  infsubc2  49050  nelsubc3lem  49059  dfswapf2  49250  isthinc  49408  cnelsubclem  49592  lanrcl  49610  ranrcl  49611  rellan  49612  relran  49613