| 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 6905 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹‘〈𝐴, 𝐵〉) = (𝐺‘〈𝐴, 𝐵〉)) | |
| 2 | df-ov 7434 | . 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | |
| 3 | df-ov 7434 | . 2 ⊢ (𝐴𝐺𝐵) = (𝐺‘〈𝐴, 𝐵〉) | |
| 4 | 1, 2, 3 | 3eqtr4g 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 |