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

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

Proof of Theorem oveq
StepHypRef Expression
1 fveq1 6147 . 2 (𝐹 = 𝐺 → (𝐹‘⟨𝐴, 𝐵⟩) = (𝐺‘⟨𝐴, 𝐵⟩))
2 df-ov 6607 . 2 (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3 df-ov 6607 . 2 (𝐴𝐺𝐵) = (𝐺‘⟨𝐴, 𝐵⟩)
41, 2, 33eqtr4g 2680 1 (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  cop 4154  cfv 5847  (class class class)co 6604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-uni 4403  df-br 4614  df-iota 5810  df-fv 5855  df-ov 6607
This theorem is referenced by:  oveqi  6617  oveqd  6621  ifov  6693  ovmpt2df  6745  ovmpt2dv2  6747  seqomeq12  7494  mapxpen  8070  seqeq2  12745  relexp0g  13696  relexpsucnnr  13699  ismgm  17164  issgrp  17206  ismnddef  17217  grpissubg  17535  isga  17645  islmod  18788  lmodfopne  18822  mamuval  20111  dmatel  20218  dmatmulcl  20225  scmate  20235  scmateALT  20237  mvmulval  20268  marrepval0  20286  marepvval0  20291  submaval0  20305  mdetleib  20312  mdetleib1  20316  mdet0pr  20317  mdetunilem1  20337  maduval  20363  minmar1val0  20372  cpmatel  20435  mat2pmatval  20448  cpm2mval  20474  decpmatval0  20488  pmatcollpw3lem  20507  mptcoe1matfsupp  20526  mp2pm2mplem4  20533  chpscmat  20566  ispsmet  22019  ismet  22038  isxmet  22039  ishtpy  22679  isphtpy  22688  isgrpo  27197  gidval  27212  grpoinvfval  27222  isablo  27246  vciOLD  27262  isvclem  27278  isnvlem  27311  isphg  27518  ofceq  29937  cvmlift2lem13  31002  ismtyval  33228  isass  33274  isexid  33275  elghomlem1OLD  33313  iscom2  33423  iscllaw  41110  iscomlaw  41111  isasslaw  41113  isrng  41161  dmatALTbasel  41476
  Copyright terms: Public domain W3C validator