| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > seqeq3d | Structured version Visualization version GIF version | ||
| Description: Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
| Ref | Expression |
|---|---|
| seqeqd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| seqeq3d | ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | seqeqd.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | seqeq3 14047 | . 2 ⊢ (𝐴 = 𝐵 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 seqcseq 14042 |
| 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-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-xp 5691 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-iota 6514 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-seq 14043 |
| This theorem is referenced by: seqeq123d 14051 seqf1olem2 14083 seqf1o 14084 seqof2 14101 expval 14104 relexp1g 15065 sumeq1 15725 sumeq2w 15728 cbvsum 15731 cbvsumv 15732 sumeq2sdv 15739 summo 15753 fsum 15756 geomulcvg 15912 prodeq1f 15942 prodeq1 15943 prodeq2w 15946 prodeq2sdv 15959 prodmo 15972 fprod 15977 gsumvalx 18689 mulgval 19089 gsumval3eu 19922 gsumval3lem2 19924 gsumzres 19927 gsumzf1o 19930 elovolmr 25511 ovolctb 25525 ovoliunlem3 25539 ovoliunnul 25542 ovolshftlem1 25544 voliunlem3 25587 voliun 25589 uniioombllem2 25618 vitalilem4 25646 vitalilem5 25647 dvnfval 25958 mtestbdd 26448 radcnv0 26459 radcnvlt1 26461 radcnvle 26463 psercn 26470 pserdvlem2 26472 abelthlem1 26475 abelthlem3 26477 logtayl 26702 atantayl2 26981 atantayl3 26982 lgamgulm2 27079 lgamcvglem 27083 lgsval 27345 lgsval4 27361 lgsneg 27365 lgsmod 27367 dchrmusumlema 27537 dchrisum0lema 27558 faclim 35746 prodeq12sdv 36219 cbvsumdavw 36280 cbvproddavw 36281 cbvsumdavw2 36296 cbvproddavw2 36297 knoppcnlem9 36502 knoppndvlem4 36516 ovoliunnfl 37669 voliunnfl 37671 radcnvrat 44333 dvradcnv2 44366 binomcxplemcvg 44373 binomcxplemdvsum 44374 binomcxplemnotnn0 44375 sumnnodd 45645 stirlinglem5 46093 sge0isummpt2 46447 ovolval2lem 46658 |
| Copyright terms: Public domain | W3C validator |