# Metamath Proof Explorer

## Theorem etransclem11

Description: A change of bound variable, often used in proofs for etransc . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Assertion etransclem11
`|- ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } ) = ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )`

### Proof

Step Hyp Ref Expression
1 oveq2
` |-  ( n = m -> ( 0 ... n ) = ( 0 ... m ) )`
2 1 oveq1d
` |-  ( n = m -> ( ( 0 ... n ) ^m ( 0 ... M ) ) = ( ( 0 ... m ) ^m ( 0 ... M ) ) )`
3 2 rabeqdv
` |-  ( n = m -> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } = { c e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )`
4 fveq2
` |-  ( j = k -> ( c ` j ) = ( c ` k ) )`
5 4 cbvsumv
` |-  sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ k e. ( 0 ... M ) ( c ` k )`
6 fveq1
` |-  ( c = d -> ( c ` k ) = ( d ` k ) )`
7 6 sumeq2sdv
` |-  ( c = d -> sum_ k e. ( 0 ... M ) ( c ` k ) = sum_ k e. ( 0 ... M ) ( d ` k ) )`
8 5 7 syl5eq
` |-  ( c = d -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ k e. ( 0 ... M ) ( d ` k ) )`
9 8 eqeq1d
` |-  ( c = d -> ( sum_ j e. ( 0 ... M ) ( c ` j ) = n <-> sum_ k e. ( 0 ... M ) ( d ` k ) = n ) )`
10 9 cbvrabv
` |-  { c e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } = { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = n }`
11 eqeq2
` |-  ( n = m -> ( sum_ k e. ( 0 ... M ) ( d ` k ) = n <-> sum_ k e. ( 0 ... M ) ( d ` k ) = m ) )`
12 11 rabbidv
` |-  ( n = m -> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = n } = { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )`
13 10 12 syl5eq
` |-  ( n = m -> { c e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } = { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )`
14 3 13 eqtrd
` |-  ( n = m -> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } = { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )`
15 14 cbvmptv
` |-  ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } ) = ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )`