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 13362 | . 2 ⊢ (𝐴 = 𝐵 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 seqcseq 13357 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-mpt 5138 df-xp 5554 df-cnv 5556 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-pred 6141 df-iota 6307 df-fv 6356 df-ov 7148 df-oprab 7149 df-mpo 7150 df-wrecs 7936 df-recs 7997 df-rdg 8035 df-seq 13358 |
This theorem is referenced by: seqeq123d 13366 seqf1olem2 13398 seqf1o 13399 seqof2 13416 expval 13419 relexp1g 14373 sumeq1 15033 sumeq2w 15037 cbvsum 15040 summo 15062 fsum 15065 geomulcvg 15220 prodeq1f 15250 prodeq2w 15254 prodmo 15278 fprod 15283 gsumvalx 17874 mulgval 18166 gsumval3eu 18953 gsumval3lem2 18955 gsumzres 18958 gsumzf1o 18961 elovolmr 24004 ovolctb 24018 ovoliunlem3 24032 ovoliunnul 24035 ovolshftlem1 24037 voliunlem3 24080 voliun 24082 uniioombllem2 24111 vitalilem4 24139 vitalilem5 24140 dvnfval 24446 mtestbdd 24920 radcnv0 24931 radcnvlt1 24933 radcnvle 24935 psercn 24941 pserdvlem2 24943 abelthlem1 24946 abelthlem3 24948 logtayl 25170 atantayl2 25443 atantayl3 25444 lgamgulm2 25540 lgamcvglem 25544 lgsval 25804 lgsval4 25820 lgsneg 25824 lgsmod 25826 dchrmusumlema 25996 dchrisum0lema 26017 faclim 32875 knoppcnlem9 33737 knoppndvlem4 33751 ovoliunnfl 34815 voliunnfl 34817 radcnvrat 40523 dvradcnv2 40556 binomcxplemcvg 40563 binomcxplemdvsum 40564 binomcxplemnotnn0 40565 sumnnodd 41787 stirlinglem5 42240 sge0isummpt2 42591 ovolval2lem 42802 |
Copyright terms: Public domain | W3C validator |