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

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

Proof of Theorem oveq
StepHypRef Expression
1 fveq1 6343 . 2 (𝐹 = 𝐺 → (𝐹‘⟨𝐴, 𝐵⟩) = (𝐺‘⟨𝐴, 𝐵⟩))
2 df-ov 6808 . 2 (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3 df-ov 6808 . 2 (𝐴𝐺𝐵) = (𝐺‘⟨𝐴, 𝐵⟩)
41, 2, 33eqtr4g 2811 1 (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624  cop 4319  cfv 6041  (class class class)co 6805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rex 3048  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049  df-ov 6808
This theorem is referenced by:  oveqi  6818  oveqd  6822  ifov  6897  ovmpt2df  6949  ovmpt2dv2  6951  seqomeq12  7710  mapxpen  8283  seqeq2  12991  relexp0g  13953  relexpsucnnr  13956  ismgm  17436  issgrp  17478  ismnddef  17489  grpissubg  17807  isga  17916  islmod  19061  lmodfopne  19095  mamuval  20386  dmatel  20493  dmatmulcl  20500  scmate  20510  scmateALT  20512  mvmulval  20543  marrepval0  20561  marepvval0  20566  submaval0  20580  mdetleib  20587  mdetleib1  20591  mdet0pr  20592  mdetunilem1  20612  maduval  20638  minmar1val0  20647  cpmatel  20710  mat2pmatval  20723  cpm2mval  20749  decpmatval0  20763  pmatcollpw3lem  20782  mptcoe1matfsupp  20801  mp2pm2mplem4  20808  chpscmat  20841  ispsmet  22302  ismet  22321  isxmet  22322  ishtpy  22964  isphtpy  22973  isgrpo  27652  gidval  27667  grpoinvfval  27677  isablo  27701  vciOLD  27717  isvclem  27733  isnvlem  27766  isphg  27973  ofceq  30460  cvmlift2lem13  31596  ismtyval  33904  isass  33950  isexid  33951  elghomlem1OLD  33989  iscom2  34099  iscllaw  42327  iscomlaw  42328  isasslaw  42330  isrng  42378  dmatALTbasel  42693
  Copyright terms: Public domain W3C validator