| 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 14045 | . 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-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-seq 14043 |
| This theorem is referenced by: seqeq123d 14051 seqf1olem2 14083 bcval5 14357 bcn2 14358 seqshft 15124 iserex 15693 isershft 15700 isercoll2 15705 isumsplit 15876 cvgrat 15919 ntrivcvg 15933 ntrivcvgtail 15936 fprodser 15985 eftlub 16145 gsumval2a 18698 gsumsgrpccat 18853 mulgnndir 19121 geolim3 26381 fmul01lt1lem2 45600 stirlinglem7 46095 stirlinglem12 46100 |
| Copyright terms: Public domain | W3C validator |