Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > seqeq1d | 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 |
---|---|
seqeq1d | ⊢ (𝜑 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | seqeqd.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | seqeq1 13463 | . 2 ⊢ (𝐴 = 𝐵 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 seqcseq 13460 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-12 2179 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-ex 1787 df-nf 1791 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-rab 3062 df-v 3400 df-un 3848 df-in 3850 df-ss 3860 df-if 4415 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-br 5031 df-opab 5093 df-mpt 5111 df-xp 5531 df-cnv 5533 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6129 df-iota 6297 df-fv 6347 df-wrecs 7976 df-recs 8037 df-rdg 8075 df-seq 13461 |
This theorem is referenced by: seqeq123d 13469 seqf1olem2 13502 bcval5 13770 bcn2 13771 seqshft 14534 iserex 15106 isershft 15113 isercoll2 15118 isumsplit 15288 cvgrat 15331 ntrivcvg 15345 ntrivcvgtail 15348 fprodser 15395 eftlub 15554 gsumval2a 18011 gsumsgrpccat 18120 gsumccatOLD 18121 mulgnndir 18374 geolim3 25087 fmul01lt1lem2 42668 stirlinglem7 43163 stirlinglem12 43168 |
Copyright terms: Public domain | W3C validator |