Theorem oveq 7416

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4595  ‘cfv 6536  (class class class)co 7410

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is used by:  oveqi  7423  oveqd  7427  ifov  7511  ovmpodf  7566  ovmpodv2  7568  seqomeq12  8437  mapxpen  9127  seqeq2  14046  relexp0g  15064  relexpsucnnr  15067  cat1  18158  ismgm  18703  mgmsscl  18707  issgrp  18782  ismnddef  18798  grpissubg  19217  isga  19365  isrng  20236  islmod  20994  lmodfopne  21030  mamuval  22559  dmatel  22659  dmatmulcl  22666  scmate  22676  scmateALT  22678  mvmulval  22709  marrepval0  22727  marepvval0  22732  submaval0  22746  mdetleib  22753  mdetleib1  22757  mdet0pr  22758  mdetunilem1  22778  maduval  22804  minmar1val0  22813  cpmatel  22877  mat2pmatval  22890  cpm2mval  22916  decpmatval0  22930  pmatcollpw3lem  22949  mptcoe1matfsupp  22968  mp2pm2mplem4  22975  chpscmat  23008  ispsmet  24470  ismet  24489  isxmet  24490  ishtpy  25140  isphtpy  25149  addsval  28164  mulsval  28311  isgrpo  30858  gidval  30873  grpoinvfval  30883  isablo  30907  vciOLD  30922  isvclem  30938  isnvlem  30971  isphg  31178  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