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

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

Proof of Theorem oveq
StepHypRef Expression
1 fveq1 6102 . 2 (𝐹 = 𝐺 → (𝐹‘⟨𝐴, 𝐵⟩) = (𝐺‘⟨𝐴, 𝐵⟩))
2 df-ov 6552 . 2 (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3 df-ov 6552 . 2 (𝐴𝐺𝐵) = (𝐺‘⟨𝐴, 𝐵⟩)
41, 2, 33eqtr4g 2669 1 (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  cop 4131  cfv 5804  (class class class)co 6549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552
This theorem is referenced by:  oveqi  6562  oveqd  6566  ifov  6638  ovmpt2df  6690  ovmpt2dv2  6692  seqomeq12  7436  mapxpen  8011  seqeq2  12667  relexp0g  13610  relexpsucnnr  13613  ismgm  17066  issgrp  17108  ismnddef  17119  grpissubg  17437  isga  17547  islmod  18690  lmodfopne  18724  mamuval  20011  dmatel  20118  dmatmulcl  20125  scmate  20135  scmateALT  20137  mvmulval  20168  marrepval0  20186  marepvval0  20191  submaval0  20205  mdetleib  20212  mdetleib1  20216  mdet0pr  20217  mdetunilem1  20237  maduval  20263  minmar1val0  20272  cpmatel  20335  mat2pmatval  20348  cpm2mval  20374  decpmatval0  20388  pmatcollpw3lem  20407  mptcoe1matfsupp  20426  mp2pm2mplem4  20433  chpscmat  20466  ispsmet  21919  ismet  21938  isxmet  21939  ishtpy  22579  isphtpy  22588  isgrpo  26735  gidval  26750  grpoinvfval  26760  isablo  26784  vciOLD  26800  isvclem  26816  isnvlem  26849  isphg  27056  ofceq  29486  cvmlift2lem13  30551  ismtyval  32769  isass  32815  isexid  32816  elghomlem1OLD  32854  iscom2  32964  iscllaw  41615  iscomlaw  41616  isasslaw  41618  isrng  41666  dmatALTbasel  41985
  Copyright terms: Public domain W3C validator