Theorem oveq 7404

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

Syntax hints:   → wi 4   = wceq 1562  ⟨cop 4590  ‘cfv 6523  (class class class)co 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-ov 7401

This theorem is referenced by:  oveqi  7411  oveqd  7415  ifov  7499  ovmpodf  7554  ovmpodv2  7556  seqomeq12  8427  mapxpen  9117  seqeq2  14020  relexp0g  15037  relexpsucnnr  15040  cat1  18132  ismgm  18677  mgmsscl  18681  issgrp  18756  ismnddef  18772  grpissubg  19190  isga  19333  isrng  20202  islmod  20933  lmodfopne  20969  mamuval  22455  dmatel  22555  dmatmulcl  22562  scmate  22572  scmateALT  22574  mvmulval  22605  marrepval0  22623  marepvval0  22628  submaval0  22642  mdetleib  22649  mdetleib1  22653  mdet0pr  22654  mdetunilem1  22674  maduval  22700  minmar1val0  22709  cpmatel  22773  mat2pmatval  22786  cpm2mval  22812  decpmatval0  22826  pmatcollpw3lem  22845  mptcoe1matfsupp  22864  mp2pm2mplem4  22871  chpscmat  22904  ispsmet  24366  ismet  24385  isxmet  24386  ishtpy  25036  isphtpy  25045  addsval  28057  mulsval  28204  isgrpo  30702  gidval  30717  grpoinvfval  30727  isablo  30751  vciOLD  30766  isvclem  30782  isnvlem  30815  isphg  31022  fxpval  33347  ofceq  34396  cvmlift2lem13  35670  nmulprop  36545  ismtyval  38304  isass  38350  isexid  38351  elghomlem1OLD  38389  iscom2  38499  iscllaw  48816  iscomlaw  48817  isasslaw  48819  dmatALTbasel  49029  infsubc2  49687  nelsubc3lem  49696  dfswapf2  49887  isthinc  50045  cnelsubclem  50229  lanrcl  50247  ranrcl  50248  rellan  50249  relran  50250