Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > oveq | Structured version Visualization version GIF version |
Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Ref | Expression |
---|---|
oveq | ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq1 6102 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹‘〈𝐴, 𝐵〉) = (𝐺‘〈𝐴, 𝐵〉)) | |
2 | df-ov 6552 | . 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | |
3 | df-ov 6552 | . 2 ⊢ (𝐴𝐺𝐵) = (𝐺‘〈𝐴, 𝐵〉) | |
4 | 1, 2, 3 | 3eqtr4g 2669 | 1 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 〈cop 4131 ‘cfv 5804 (class class class)co 6549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-ov 6552 |
This theorem is referenced by: oveqi 6562 oveqd 6566 ifov 6638 ovmpt2df 6690 ovmpt2dv2 6692 seqomeq12 7436 mapxpen 8011 seqeq2 12667 relexp0g 13610 relexpsucnnr 13613 ismgm 17066 issgrp 17108 ismnddef 17119 grpissubg 17437 isga 17547 islmod 18690 lmodfopne 18724 mamuval 20011 dmatel 20118 dmatmulcl 20125 scmate 20135 scmateALT 20137 mvmulval 20168 marrepval0 20186 marepvval0 20191 submaval0 20205 mdetleib 20212 mdetleib1 20216 mdet0pr 20217 mdetunilem1 20237 maduval 20263 minmar1val0 20272 cpmatel 20335 mat2pmatval 20348 cpm2mval 20374 decpmatval0 20388 pmatcollpw3lem 20407 mptcoe1matfsupp 20426 mp2pm2mplem4 20433 chpscmat 20466 ispsmet 21919 ismet 21938 isxmet 21939 ishtpy 22579 isphtpy 22588 isgrpo 26735 gidval 26750 grpoinvfval 26760 isablo 26784 vciOLD 26800 isvclem 26816 isnvlem 26849 isphg 27056 ofceq 29486 cvmlift2lem13 30551 ismtyval 32769 isass 32815 isexid 32816 elghomlem1OLD 32854 iscom2 32964 iscllaw 41615 iscomlaw 41616 isasslaw 41618 isrng 41666 dmatALTbasel 41985 |
Copyright terms: Public domain | W3C validator |