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

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

Proof of Theorem oveq
StepHypRef Expression
1 fveq1 6905 . 2 (𝐹 = 𝐺 → (𝐹‘⟨𝐴, 𝐵⟩) = (𝐺‘⟨𝐴, 𝐵⟩))
2 df-ov 7434 . 2 (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3 df-ov 7434 . 2 (𝐴𝐺𝐵) = (𝐺‘⟨𝐴, 𝐵⟩)
41, 2, 33eqtr4g 2802 1 (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  cop 4632  cfv 6561  (class class class)co 7431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434
This theorem is referenced by:  oveqi  7444  oveqd  7448  ifov  7534  ovmpodf  7589  ovmpodv2  7591  seqomeq12  8494  mapxpen  9183  seqeq2  14046  relexp0g  15061  relexpsucnnr  15064  cat1  18142  ismgm  18654  mgmsscl  18658  issgrp  18733  ismnddef  18749  grpissubg  19164  isga  19309  isrng  20151  islmod  20862  lmodfopne  20898  mamuval  22397  dmatel  22499  dmatmulcl  22506  scmate  22516  scmateALT  22518  mvmulval  22549  marrepval0  22567  marepvval0  22572  submaval0  22586  mdetleib  22593  mdetleib1  22597  mdet0pr  22598  mdetunilem1  22618  maduval  22644  minmar1val0  22653  cpmatel  22717  mat2pmatval  22730  cpm2mval  22756  decpmatval0  22770  pmatcollpw3lem  22789  mptcoe1matfsupp  22808  mp2pm2mplem4  22815  chpscmat  22848  ispsmet  24314  ismet  24333  isxmet  24334  ishtpy  25004  isphtpy  25013  addsval  27995  mulsval  28135  isgrpo  30516  gidval  30531  grpoinvfval  30541  isablo  30565  vciOLD  30580  isvclem  30596  isnvlem  30629  isphg  30836  ofceq  34098  cvmlift2lem13  35320  ismtyval  37807  isass  37853  isexid  37854  elghomlem1OLD  37892  iscom2  38002  iscllaw  48105  iscomlaw  48106  isasslaw  48108  dmatALTbasel  48319  dfswapf2  48967  isthinc  49069
  Copyright terms: Public domain W3C validator