Theorem oveq 7437

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4632  ‘cfv 6561  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  oveqi  7444  oveqd  7448  ifov  7534  ovmpodf  7589  ovmpodv2  7591  seqomeq12  8494  mapxpen  9183  seqeq2  14046  relexp0g  15061  relexpsucnnr  15064  cat1  18142  ismgm  18654  mgmsscl  18658  issgrp  18733  ismnddef  18749  grpissubg  19164  isga  19309  isrng  20151  islmod  20862  lmodfopne  20898  mamuval  22397  dmatel  22499  dmatmulcl  22506  scmate  22516  scmateALT  22518  mvmulval  22549  marrepval0  22567  marepvval0  22572  submaval0  22586  mdetleib  22593  mdetleib1  22597  mdet0pr  22598  mdetunilem1  22618  maduval  22644  minmar1val0  22653  cpmatel  22717  mat2pmatval  22730  cpm2mval  22756  decpmatval0  22770  pmatcollpw3lem  22789  mptcoe1matfsupp  22808  mp2pm2mplem4  22815  chpscmat  22848  ispsmet  24314  ismet  24333  isxmet  24334  ishtpy  25004  isphtpy  25013  addsval  27995  mulsval  28135  isgrpo  30516  gidval  30531  grpoinvfval  30541  isablo  30565  vciOLD  30580  isvclem  30596  isnvlem  30629  isphg  30836  ofceq  34098  cvmlift2lem13  35320  ismtyval  37807  isass  37853  isexid  37854  elghomlem1OLD  37892  iscom2  38002  iscllaw  48105  iscomlaw  48106  isasslaw  48108  dmatALTbasel  48319  dfswapf2  48967  isthinc  49069