Theorem oveq 7454

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

Syntax hints:   → wi 4   = wceq 1537  ⟨cop 4654  ‘cfv 6573  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  oveqi  7461  oveqd  7465  ifov  7551  ovmpodf  7606  ovmpodv2  7608  seqomeq12  8510  mapxpen  9209  seqeq2  14056  relexp0g  15071  relexpsucnnr  15074  cat1  18164  ismgm  18679  mgmsscl  18683  issgrp  18758  ismnddef  18774  grpissubg  19186  isga  19331  isrng  20181  islmod  20884  lmodfopne  20920  mamuval  22418  dmatel  22520  dmatmulcl  22527  scmate  22537  scmateALT  22539  mvmulval  22570  marrepval0  22588  marepvval0  22593  submaval0  22607  mdetleib  22614  mdetleib1  22618  mdet0pr  22619  mdetunilem1  22639  maduval  22665  minmar1val0  22674  cpmatel  22738  mat2pmatval  22751  cpm2mval  22777  decpmatval0  22791  pmatcollpw3lem  22810  mptcoe1matfsupp  22829  mp2pm2mplem4  22836  chpscmat  22869  ispsmet  24335  ismet  24354  isxmet  24355  ishtpy  25023  isphtpy  25032  addsval  28013  mulsval  28153  isgrpo  30529  gidval  30544  grpoinvfval  30554  isablo  30578  vciOLD  30593  isvclem  30609  isnvlem  30642  isphg  30849  ofceq  34061  cvmlift2lem13  35283  ismtyval  37760  isass  37806  isexid  37807  elghomlem1OLD  37845  iscom2  37955  iscllaw  47912  iscomlaw  47913  isasslaw  47915  dmatALTbasel  48131  isthinc  48688