Description: The second class argument to a sum can be chosen so that it is always a set. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jul-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sum2id | |- sum_ k e. A B = sum_ k e. A ( _I ` B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sumeq2ii | |- ( A. k e. A ( _I ` B ) = ( _I ` ( _I ` B ) ) -> sum_ k e. A B = sum_ k e. A ( _I ` B ) ) |
|
| 2 | fvex | |- ( _I ` B ) e. _V |
|
| 3 | fvi | |- ( ( _I ` B ) e. _V -> ( _I ` ( _I ` B ) ) = ( _I ` B ) ) |
|
| 4 | 2 3 | ax-mp | |- ( _I ` ( _I ` B ) ) = ( _I ` B ) |
| 5 | 4 | eqcomi | |- ( _I ` B ) = ( _I ` ( _I ` B ) ) |
| 6 | 5 | a1i | |- ( k e. A -> ( _I ` B ) = ( _I ` ( _I ` B ) ) ) |
| 7 | 1 6 | mprg | |- sum_ k e. A B = sum_ k e. A ( _I ` B ) |