MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveq Structured version   Visualization version   GIF version

Theorem oveq 7364
Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
oveq (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))

Proof of Theorem oveq
StepHypRef Expression
1 fveq1 6842 . 2 (𝐹 = 𝐺 → (𝐹‘⟨𝐴, 𝐵⟩) = (𝐺‘⟨𝐴, 𝐵⟩))
2 df-ov 7361 . 2 (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3 df-ov 7361 . 2 (𝐴𝐺𝐵) = (𝐺‘⟨𝐴, 𝐵⟩)
41, 2, 33eqtr4g 2802 1 (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  cop 4593  cfv 6497  (class class class)co 7358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  oveqi  7371  oveqd  7375  ifov  7458  ovmpodf  7512  ovmpodv2  7514  seqomeq12  8401  mapxpen  9088  seqeq2  13911  relexp0g  14908  relexpsucnnr  14911  cat1  17984  ismgm  18499  mgmsscl  18503  issgrp  18548  ismnddef  18559  grpissubg  18949  isga  19072  islmod  20329  lmodfopne  20363  mamuval  21738  dmatel  21845  dmatmulcl  21852  scmate  21862  scmateALT  21864  mvmulval  21895  marrepval0  21913  marepvval0  21918  submaval0  21932  mdetleib  21939  mdetleib1  21943  mdet0pr  21944  mdetunilem1  21964  maduval  21990  minmar1val0  21999  cpmatel  22063  mat2pmatval  22076  cpm2mval  22102  decpmatval0  22116  pmatcollpw3lem  22135  mptcoe1matfsupp  22154  mp2pm2mplem4  22161  chpscmat  22194  ispsmet  23660  ismet  23679  isxmet  23680  ishtpy  24338  isphtpy  24347  addsval  27277  isgrpo  29442  gidval  29457  grpoinvfval  29467  isablo  29491  vciOLD  29506  isvclem  29522  isnvlem  29555  isphg  29762  ofceq  32699  cvmlift2lem13  33912  mulsval  34411  ismtyval  36262  isass  36308  isexid  36309  elghomlem1OLD  36347  iscom2  36457  iscllaw  46130  iscomlaw  46131  isasslaw  46133  isrng  46181  dmatALTbasel  46490  isthinc  47048
  Copyright terms: Public domain W3C validator