Theorem oveq 7415

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4590  ‘cfv 6528  (class class class)co 7409

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868  df-br 5104  df-iota 6484  df-fv 6536  df-ov 7412

This theorem is used by:  oveqi  7422  oveqd  7426  ifov  7510  ovmpodf  7565  ovmpodv2  7567  seqomeq12  8443  mapxpen  9141  seqeq2  14102  relexp0g  15128  relexpsucnnr  15131  cat1  18219  ismgm  18764  mgmsscl  18768  issgrp  18856  ismnddef  18872  grpissubg  19304  isga  19452  isrng  20323  islmod  21086  lmodfopne  21122  mamuval  22655  dmatel  22755  dmatmulcl  22762  scmate  22772  scmateALT  22774  mvmulval  22805  marrepval0  22823  marepvval0  22828  submaval0  22842  mdetleib  22849  mdetleib1  22853  mdet0pr  22854  mdetunilem1  22874  maduval  22900  minmar1val0  22909  cpmatel  22976  mat2pmatval  22989  cpm2mval  23015  decpmatval0  23029  pmatcollpw3lem  23048  mptcoe1matfsupp  23067  mp2pm2mplem4  23074  chpscmat  23107  ispsmet  24570  ismet  24589  isxmet  24590  ishtpy  25240  isphtpy  25249  addsval  28267  mulsval  28414  isgrpo  31018  gidval  31033  grpoinvfval  31043  isablo  31067  vciOLD  31082  isvclem  31098  isnvlem  31131  isphg  31338  fxpval  33645  ofceq  34648  cvmlift2lem13  35995  nmulprop  36855  ismtyval  38648  isass  38694  isexid  38695  elghomlem1OLD  38733  iscom2  38843  iscllaw  49202  iscomlaw  49203  isasslaw  49205  dmatALTbasel  49430  infsubc2  50085  nelsubc3lem  50094  dfswapf2  50285  isthinc  50443  cnelsubclem  50627  lanrcl  50645  ranrcl  50646  rellan  50647  relran  50648