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

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

Proof of Theorem oveq
StepHypRef Expression
1 fveq1 6668 . 2 (𝐹 = 𝐺 → (𝐹‘⟨𝐴, 𝐵⟩) = (𝐺‘⟨𝐴, 𝐵⟩))
2 df-ov 7153 . 2 (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3 df-ov 7153 . 2 (𝐴𝐺𝐵) = (𝐺‘⟨𝐴, 𝐵⟩)
41, 2, 33eqtr4g 2886 1 (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  cop 4570  cfv 6354  (class class class)co 7150
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-rex 3149  df-uni 4838  df-br 5064  df-iota 6313  df-fv 6362  df-ov 7153
This theorem is referenced by:  oveqi  7163  oveqd  7167  ifov  7248  ovmpodf  7300  ovmpodv2  7302  seqomeq12  8086  mapxpen  8677  seqeq2  13368  relexp0g  14376  relexpsucnnr  14379  ismgm  17848  mgmsscl  17852  issgrp  17897  ismnddef  17908  grpissubg  18244  isga  18366  islmod  19574  lmodfopne  19608  mamuval  20932  dmatel  21037  dmatmulcl  21044  scmate  21054  scmateALT  21056  mvmulval  21087  marrepval0  21105  marepvval0  21110  submaval0  21124  mdetleib  21131  mdetleib1  21135  mdet0pr  21136  mdetunilem1  21156  maduval  21182  minmar1val0  21191  cpmatel  21254  mat2pmatval  21267  cpm2mval  21293  decpmatval0  21307  pmatcollpw3lem  21326  mptcoe1matfsupp  21345  mp2pm2mplem4  21352  chpscmat  21385  ispsmet  22848  ismet  22867  isxmet  22868  ishtpy  23510  isphtpy  23519  isgrpo  28207  gidval  28222  grpoinvfval  28232  isablo  28256  vciOLD  28271  isvclem  28287  isnvlem  28320  isphg  28527  ofceq  31261  cvmlift2lem13  32465  ismtyval  34965  isass  35011  isexid  35012  elghomlem1OLD  35050  iscom2  35160  iscllaw  43998  iscomlaw  43999  isasslaw  44001  isrng  44049  dmatALTbasel  44359
  Copyright terms: Public domain W3C validator