Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > oveq | Structured version Visualization version Unicode version |
Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Ref | Expression |
---|---|
oveq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq1 6190 | . 2 | |
2 | df-ov 6653 | . 2 | |
3 | df-ov 6653 | . 2 | |
4 | 1, 2, 3 | 3eqtr4g 2681 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 cop 4183 cfv 5888 (class class class)co 6650 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 |
This theorem is referenced by: oveqi 6663 oveqd 6667 ifov 6740 ovmpt2df 6792 ovmpt2dv2 6794 seqomeq12 7549 mapxpen 8126 seqeq2 12805 relexp0g 13762 relexpsucnnr 13765 ismgm 17243 issgrp 17285 ismnddef 17296 grpissubg 17614 isga 17724 islmod 18867 lmodfopne 18901 mamuval 20192 dmatel 20299 dmatmulcl 20306 scmate 20316 scmateALT 20318 mvmulval 20349 marrepval0 20367 marepvval0 20372 submaval0 20386 mdetleib 20393 mdetleib1 20397 mdet0pr 20398 mdetunilem1 20418 maduval 20444 minmar1val0 20453 cpmatel 20516 mat2pmatval 20529 cpm2mval 20555 decpmatval0 20569 pmatcollpw3lem 20588 mptcoe1matfsupp 20607 mp2pm2mplem4 20614 chpscmat 20647 ispsmet 22109 ismet 22128 isxmet 22129 ishtpy 22771 isphtpy 22780 isgrpo 27351 gidval 27366 grpoinvfval 27376 isablo 27400 vciOLD 27416 isvclem 27432 isnvlem 27465 isphg 27672 ofceq 30159 cvmlift2lem13 31297 ismtyval 33599 isass 33645 isexid 33646 elghomlem1OLD 33684 iscom2 33794 iscllaw 41825 iscomlaw 41826 isasslaw 41828 isrng 41876 dmatALTbasel 42191 |
Copyright terms: Public domain | W3C validator |