Theorem oveq 7418

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ⟨cop 4594  ‘cfv 6536  (class class class)co 7412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7415

This theorem is used by:  oveqi  7425  oveqd  7429  ifov  7513  ovmpodf  7568  ovmpodv2  7570  seqomeq12  8439  mapxpen  9129  seqeq2  14048  relexp0g  15066  relexpsucnnr  15069  cat1  18160  ismgm  18705  mgmsscl  18709  issgrp  18784  ismnddef  18800  grpissubg  19219  isga  19367  isrng  20238  islmod  20996  lmodfopne  21032  mamuval  22561  dmatel  22661  dmatmulcl  22668  scmate  22678  scmateALT  22680  mvmulval  22711  marrepval0  22729  marepvval0  22734  submaval0  22748  mdetleib  22755  mdetleib1  22759  mdet0pr  22760  mdetunilem1  22780  maduval  22806  minmar1val0  22815  cpmatel  22879  mat2pmatval  22892  cpm2mval  22918  decpmatval0  22932  pmatcollpw3lem  22951  mptcoe1matfsupp  22970  mp2pm2mplem4  22977  chpscmat  23010  ispsmet  24472  ismet  24491  isxmet  24492  ishtpy  25142  isphtpy  25151  addsval  28166  mulsval  28313  isgrpo  30860  gidval  30875  grpoinvfval  30885  isablo  30909  vciOLD  30924  isvclem  30940  isnvlem  30973  isphg  31180  fxpval  33494  ofceq  34496  cvmlift2lem13  35815  nmulprop  36690  ismtyval  38479  isass  38525  isexid  38526  elghomlem1OLD  38564  iscom2  38674  iscllaw  48982  iscomlaw  48983  isasslaw  48985  dmatALTbasel  49210  infsubc2  49867  nelsubc3lem  49876  dfswapf2  50067  isthinc  50225  cnelsubclem  50409  lanrcl  50427  ranrcl  50428  rellan  50429  relran  50430