Description: A lemma to facilitate conversions from the function form to the class-variable form of a sum. (Contributed by Mario Carneiro, 12-Aug-2013) (Revised by Mario Carneiro, 23-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | sumfc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | 1 | fvmpt2i | |
3 | 2 | sumeq2i | |
4 | nffvmpt1 | |
|
5 | nfcv | |
|
6 | fveq2 | |
|
7 | 4 5 6 | cbvsumi | |
8 | sum2id | |
|
9 | 3 7 8 | 3eqtr4i | |