Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > seqeq1 | Unicode version |
Description: Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
Ref | Expression |
---|---|
seqeq1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . . . . . 6 | |
2 | fveq2 5494 | . . . . . 6 | |
3 | 1, 2 | opeq12d 3771 | . . . . 5 |
4 | freceq2 6369 | . . . . 5 frec frec | |
5 | 3, 4 | syl 14 | . . . 4 frec frec |
6 | fveq2 5494 | . . . . . 6 | |
7 | eqid 2170 | . . . . . 6 | |
8 | mpoeq12 5910 | . . . . . 6 | |
9 | 6, 7, 8 | sylancl 411 | . . . . 5 |
10 | freceq1 6368 | . . . . 5 frec frec | |
11 | 9, 10 | syl 14 | . . . 4 frec frec |
12 | 5, 11 | eqtrd 2203 | . . 3 frec frec |
13 | 12 | rneqd 4838 | . 2 frec frec |
14 | df-seqfrec 10389 | . 2 frec | |
15 | df-seqfrec 10389 | . 2 frec | |
16 | 13, 14, 15 | 3eqtr4g 2228 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1348 cvv 2730 cop 3584 crn 4610 cfv 5196 (class class class)co 5850 cmpo 5852 freccfrec 6366 c1 7762 caddc 7764 cuz 9474 cseq 10388 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-rex 2454 df-v 2732 df-un 3125 df-in 3127 df-ss 3134 df-sn 3587 df-pr 3588 df-op 3590 df-uni 3795 df-br 3988 df-opab 4049 df-mpt 4050 df-cnv 4617 df-dm 4619 df-rn 4620 df-res 4621 df-iota 5158 df-fv 5204 df-oprab 5854 df-mpo 5855 df-recs 6281 df-frec 6367 df-seqfrec 10389 |
This theorem is referenced by: seqeq1d 10394 seq3f1olemqsum 10443 seq3id 10451 seq3z 10454 iserex 11289 summodclem2 11332 summodc 11333 zsumdc 11334 isumsplit 11441 ntrivcvgap 11498 ntrivcvgap0 11499 prodmodclem2 11527 prodmodc 11528 zproddc 11529 fprodntrivap 11534 ege2le3 11621 |
Copyright terms: Public domain | W3C validator |