Theorem oveq 7422

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4593  ‘cfv 6537  (class class class)co 7416

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419

This theorem is used by:  oveqi  7429  oveqd  7433  ifov  7517  ovmpodf  7572  ovmpodv2  7574  seqomeq12  8446  mapxpen  9144  seqeq2  14071  relexp0g  15097  relexpsucnnr  15100  cat1  18190  ismgm  18735  mgmsscl  18739  issgrp  18824  ismnddef  18840  grpissubg  19271  isga  19419  isrng  20290  islmod  21049  lmodfopne  21085  mamuval  22616  dmatel  22716  dmatmulcl  22723  scmate  22733  scmateALT  22735  mvmulval  22766  marrepval0  22784  marepvval0  22789  submaval0  22803  mdetleib  22810  mdetleib1  22814  mdet0pr  22815  mdetunilem1  22835  maduval  22861  minmar1val0  22870  cpmatel  22937  mat2pmatval  22950  cpm2mval  22976  decpmatval0  22990  pmatcollpw3lem  23009  mptcoe1matfsupp  23028  mp2pm2mplem4  23035  chpscmat  23068  ispsmet  24531  ismet  24550  isxmet  24551  ishtpy  25201  isphtpy  25210  addsval  28225  mulsval  28372  isgrpo  30964  gidval  30979  grpoinvfval  30989  isablo  31013  vciOLD  31028  isvclem  31044  isnvlem  31077  isphg  31284  fxpval  33592  ofceq  34594  cvmlift2lem13  35881  nmulprop  36757  ismtyval  38537  isass  38583  isexid  38584  elghomlem1OLD  38622  iscom2  38732  iscllaw  49091  iscomlaw  49092  isasslaw  49094  dmatALTbasel  49319  infsubc2  49974  nelsubc3lem  49983  dfswapf2  50174  isthinc  50332  cnelsubclem  50516  lanrcl  50534  ranrcl  50535  rellan  50536  relran  50537