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

Theorem oveq 6302
Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
oveq

Proof of Theorem oveq
StepHypRef Expression
1 fveq1 5870 . 2
2 df-ov 6299 . 2
3 df-ov 6299 . 2
41, 2, 33eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  <.cop 4035  `cfv 5593  (class class class)co 6296
This theorem is referenced by:  oveqi  6309  oveqd  6313  ifov  6382  ovmpt2df  6434  ovmpt2dv2  6436  seqomeq12  7138  mapxpen  7703  seqeq2  12111  ismgm  15873  issgrp  15912  ismnddef  15922  grpissubg  16221  isga  16329  islmod  17516  mamuval  18888  dmatel  18995  dmatmulcl  19002  scmate  19012  scmateALT  19014  mvmulval  19045  marrepval0  19063  marepvval0  19068  submaval0  19082  mdetleib  19089  mdetleib1  19093  mdet0pr  19094  mdetunilem1  19114  maduval  19140  minmar1val0  19149  cpmatel  19212  mat2pmatval  19225  cpm2mval  19251  decpmatval0  19265  pmatcollpw3lem  19284  mptcoe1matfsupp  19303  mp2pm2mplem4  19310  chpscmat  19343  ispsmet  20808  ismet  20826  isxmet  20827  ishtpy  21472  isphtpy  21481  isgrpo  25198  gidval  25215  grpoinvfval  25226  isablo  25285  isass  25318  isexid  25319  elghomlem1OLD  25363  iscom2  25414  vci  25441  isvclem  25470  isnvlem  25503  isphg  25732  ofceq  28096  cvmlift2lem13  28760  relexp0  29052  relexpsucr  29053  ismtyval  30296  iscllaw  32513  iscomlaw  32514  isasslaw  32516  isrng  32682  dmatALTbasel  33003
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299
  Copyright terms: Public domain W3C validator