| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > oveqdr | Structured version Visualization version GIF version | ||
| Description: Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.) |
| Ref | Expression |
|---|---|
| oveqdr.1 | ⊢ (𝜑 → 𝐹 = 𝐺) |
| Ref | Expression |
|---|---|
| oveqdr | ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oveqdr.1 | . . 3 ⊢ (𝜑 → 𝐹 = 𝐺) | |
| 2 | 1 | oveqd 7448 | . 2 ⊢ (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) |
| 3 | 2 | adantr 480 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 (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: fullresc 17896 fucpropd 18025 resssetc 18137 resscatc 18154 issstrmgm 18666 gsumpropd 18691 issubmgm2 18716 grpsubpropd 19063 sylow2blem2 19639 isrngd 20170 prdsrngd 20173 isringd 20288 prdsringd 20318 prdscrngd 20319 prds1 20320 rnghmval 20440 pwsco1rhm 20502 pwsco2rhm 20503 pwsdiagrhm 20607 rnghmsubcsetclem1 20631 rnghmsubcsetclem2 20632 rngcifuestrc 20639 rhmsubcsetclem1 20660 rhmsubcsetclem2 20661 rhmsubcrngclem1 20666 rhmsubcrngclem2 20667 isdomn 20705 primefld 20806 sraring 21193 sralmod 21194 sralmod0 21195 issubrgd 21196 znzrh 21561 zncrng 21563 phlssphl 21677 sraassaOLD 21890 opsrcrng 22083 opsrassa 22084 ply1lss 22198 ply1subrg 22199 opsr0 22220 opsr1 22221 subrgply1 22234 opsrring 22246 opsrlmod 22247 ply1mpl0 22258 ply1mpl1 22260 ply1ascl 22261 coe1tm 22276 evls1rhm 22326 evl1rhm 22336 evl1expd 22349 evls1maplmhm 22381 mat0 22423 matinvg 22424 matlmod 22435 scmatsrng1 22529 1mavmul 22554 mat2pmatmul 22737 ressprdsds 24381 nmpropd 24607 tng0 24659 tngngp2 24673 tnggrpr 24676 tngnrg 24695 sranlm 24705 pi1addval 25081 cvsi 25163 tcphphl 25261 abvpropd2 32950 resv0g 33367 resvcmn 33369 sra1r 33632 sradrng 33633 sraidom 33634 srasubrg 33635 drgextlsp 33644 tnglvec 33663 tngdim 33664 matdim 33666 fedgmullem2 33681 fldextrspunfld 33726 zhmnrg 33966 prdsbnd 37800 prdstotbnd 37801 prdsbnd2 37802 erngdvlem3 40992 erngdvlem3-rN 41000 hlhils0 41951 hlhils1N 41952 hlhillvec 41957 hlhildrng 41958 hlhil0 41961 hlhillsm 41962 zndvdchrrhm 41972 isprimroot 42094 primrootsunit1 42098 mendval 43191 mnring0gd 44238 mnringlmodd 44245 ovmpt4d 48768 upfval 48933 |
| Copyright terms: Public domain | W3C validator |