![]() |
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 13967 | . 2 ⊢ (𝐴 = 𝐵 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 seqcseq 13962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-xp 5681 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-iota 6492 df-fv 6548 df-ov 7407 df-oprab 7408 df-mpo 7409 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-seq 13963 |
This theorem is referenced by: seqeq123d 13971 seqf1olem2 14004 seqf1o 14005 seqof2 14022 expval 14025 relexp1g 14969 sumeq1 15631 sumeq2w 15634 cbvsum 15637 summo 15659 fsum 15662 geomulcvg 15818 prodeq1f 15848 prodeq2w 15852 prodmo 15876 fprod 15881 gsumvalx 18591 mulgval 18948 gsumval3eu 19764 gsumval3lem2 19766 gsumzres 19769 gsumzf1o 19772 elovolmr 24975 ovolctb 24989 ovoliunlem3 25003 ovoliunnul 25006 ovolshftlem1 25008 voliunlem3 25051 voliun 25053 uniioombllem2 25082 vitalilem4 25110 vitalilem5 25111 dvnfval 25421 mtestbdd 25899 radcnv0 25910 radcnvlt1 25912 radcnvle 25914 psercn 25920 pserdvlem2 25922 abelthlem1 25925 abelthlem3 25927 logtayl 26150 atantayl2 26423 atantayl3 26424 lgamgulm2 26520 lgamcvglem 26524 lgsval 26784 lgsval4 26800 lgsneg 26804 lgsmod 26806 dchrmusumlema 26976 dchrisum0lema 26997 faclim 34654 knoppcnlem9 35315 knoppndvlem4 35329 ovoliunnfl 36468 voliunnfl 36470 radcnvrat 43006 dvradcnv2 43039 binomcxplemcvg 43046 binomcxplemdvsum 43047 binomcxplemnotnn0 43048 sumnnodd 44281 stirlinglem5 44729 sge0isummpt2 45083 ovolval2lem 45294 |
Copyright terms: Public domain | W3C validator |