Theorem oveq 7411

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4607  ‘cfv 6531  (class class class)co 7405

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408

This theorem is referenced by:  oveqi  7418  oveqd  7422  ifov  7508  ovmpodf  7563  ovmpodv2  7565  seqomeq12  8468  mapxpen  9157  seqeq2  14023  relexp0g  15041  relexpsucnnr  15044  cat1  18110  ismgm  18619  mgmsscl  18623  issgrp  18698  ismnddef  18714  grpissubg  19129  isga  19274  isrng  20114  islmod  20821  lmodfopne  20857  mamuval  22331  dmatel  22431  dmatmulcl  22438  scmate  22448  scmateALT  22450  mvmulval  22481  marrepval0  22499  marepvval0  22504  submaval0  22518  mdetleib  22525  mdetleib1  22529  mdet0pr  22530  mdetunilem1  22550  maduval  22576  minmar1val0  22585  cpmatel  22649  mat2pmatval  22662  cpm2mval  22688  decpmatval0  22702  pmatcollpw3lem  22721  mptcoe1matfsupp  22740  mp2pm2mplem4  22747  chpscmat  22780  ispsmet  24243  ismet  24262  isxmet  24263  ishtpy  24922  isphtpy  24931  addsval  27921  mulsval  28064  isgrpo  30478  gidval  30493  grpoinvfval  30503  isablo  30527  vciOLD  30542  isvclem  30558  isnvlem  30591  isphg  30798  ofceq  34128  cvmlift2lem13  35337  ismtyval  37824  isass  37870  isexid  37871  elghomlem1OLD  37909  iscom2  38019  iscllaw  48164  iscomlaw  48165  isasslaw  48167  dmatALTbasel  48378  infsubc2  49028  nelsubc3lem  49037  dfswapf2  49178  isthinc  49305  cnelsubclem  49480  lanrcl  49496  ranrcl  49497  rellan  49498  relran  49499