Theorem oveq 7376

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

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4588  ‘cfv 6502  (class class class)co 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373

This theorem is referenced by:  oveqi  7383  oveqd  7387  ifov  7471  ovmpodf  7526  ovmpodv2  7528  seqomeq12  8397  mapxpen  9085  seqeq2  13942  relexp0g  14959  relexpsucnnr  14962  cat1  18035  ismgm  18580  mgmsscl  18584  issgrp  18659  ismnddef  18675  grpissubg  19093  isga  19237  isrng  20106  islmod  20832  lmodfopne  20868  mamuval  22354  dmatel  22454  dmatmulcl  22461  scmate  22471  scmateALT  22473  mvmulval  22504  marrepval0  22522  marepvval0  22527  submaval0  22541  mdetleib  22548  mdetleib1  22552  mdet0pr  22553  mdetunilem1  22573  maduval  22599  minmar1val0  22608  cpmatel  22672  mat2pmatval  22685  cpm2mval  22711  decpmatval0  22725  pmatcollpw3lem  22744  mptcoe1matfsupp  22763  mp2pm2mplem4  22770  chpscmat  22803  ispsmet  24265  ismet  24284  isxmet  24285  ishtpy  24944  isphtpy  24953  addsval  27975  mulsval  28122  isgrpo  30591  gidval  30606  grpoinvfval  30616  isablo  30640  vciOLD  30655  isvclem  30671  isnvlem  30704  isphg  30911  fxpval  33265  ofceq  34281  cvmlift2lem13  35537  ismtyval  38080  isass  38126  isexid  38127  elghomlem1OLD  38165  iscom2  38275  iscllaw  48578  iscomlaw  48579  isasslaw  48581  dmatALTbasel  48791  infsubc2  49449  nelsubc3lem  49458  dfswapf2  49649  isthinc  49807  cnelsubclem  49991  lanrcl  50009  ranrcl  50010  rellan  50011  relran  50012