Theorem oveq 7396

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4598  ‘cfv 6514  (class class class)co 7390

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  oveqi  7403  oveqd  7407  ifov  7493  ovmpodf  7548  ovmpodv2  7550  seqomeq12  8425  mapxpen  9113  seqeq2  13977  relexp0g  14995  relexpsucnnr  14998  cat1  18066  ismgm  18575  mgmsscl  18579  issgrp  18654  ismnddef  18670  grpissubg  19085  isga  19230  isrng  20070  islmod  20777  lmodfopne  20813  mamuval  22287  dmatel  22387  dmatmulcl  22394  scmate  22404  scmateALT  22406  mvmulval  22437  marrepval0  22455  marepvval0  22460  submaval0  22474  mdetleib  22481  mdetleib1  22485  mdet0pr  22486  mdetunilem1  22506  maduval  22532  minmar1val0  22541  cpmatel  22605  mat2pmatval  22618  cpm2mval  22644  decpmatval0  22658  pmatcollpw3lem  22677  mptcoe1matfsupp  22696  mp2pm2mplem4  22703  chpscmat  22736  ispsmet  24199  ismet  24218  isxmet  24219  ishtpy  24878  isphtpy  24887  addsval  27876  mulsval  28019  isgrpo  30433  gidval  30448  grpoinvfval  30458  isablo  30482  vciOLD  30497  isvclem  30513  isnvlem  30546  isphg  30753  fxpval  33129  ofceq  34094  cvmlift2lem13  35309  ismtyval  37801  isass  37847  isexid  37848  elghomlem1OLD  37886  iscom2  37996  iscllaw  48181  iscomlaw  48182  isasslaw  48184  dmatALTbasel  48395  infsubc2  49054  nelsubc3lem  49063  dfswapf2  49254  isthinc  49412  cnelsubclem  49596  lanrcl  49614  ranrcl  49615  rellan  49616  relran  49617