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

Theorem oveqi 6309
Description: Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
Hypothesis
Ref Expression
oveq1i.1
Assertion
Ref Expression
oveqi

Proof of Theorem oveqi
StepHypRef Expression
1 oveq1i.1 . 2
2 oveq 6302 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  (class class class)co 6296
This theorem is referenced by:  oveq123i  6310  cantnfval2  8109  cantnfval2OLD  8139  vdwap1  14495  vdwlem12  14510  prdsdsval3  14882  oppchom  15110  yonedalem21  15542  yonedalem22  15547  mndprop  15947  issubm  15978  frmdadd  16023  grpprop  16069  oppgplus  16384  ablprop  16809  ringpropd  17230  crngpropd  17231  ringprop  17232  opprmul  17275  opprringb  17281  mulgass3  17286  rngidpropd  17344  invrpropd  17347  drngprop  17407  subrgpropd  17463  rhmpropd  17464  lidlacl  17860  lidlmcl  17865  lidlrsppropd  17878  crngridl  17886  psradd  18035  ressmpladd  18119  ressmplmul  18120  ressmplvsca  18121  ressply1add  18271  ressply1mul  18272  ressply1vsca  18273  ply1coe  18337  ply1coeOLD  18338  scmatscmiddistr  19010  1marepvsma1  19085  decpmatmulsumfsupp  19274  pmatcollpw1lem2  19276  pmatcollpwscmatlem1  19290  mptcoe1matfsupp  19303  mp2pm2mplem4  19310  chmatval  19330  chpidmat  19348  xpsdsval  20884  blres  20934  nmfval2  21111  nmval2  21112  cncfmet  21412  minveclem2  21841  minveclem3b  21843  minveclem4  21847  minveclem6  21849  ply1divalg2  22539  issubgoi  25312  ghgrplem2OLD  25369  nvm  25536  xrge0pluscn  27922  esumpfinvallem  28080  equivbnd2  30288  ismtyres  30304  iccbnd  30336  exidreslem  30339  iscrngo2  30395  mendplusgfval  31134  issubmgm  32477  rcaninv  32578  initoeu2lem0  32619  rhmsubclem4  32897  zlmodzxzadd  32947  snlindsntor  33072  toycom  34698
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