# Metamath Proof Explorer

## Theorem etransclem5

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

Ref Expression
Assertion etransclem5 ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦𝑋 ↦ ( ( 𝑦𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )

### Proof

Step Hyp Ref Expression
1 oveq1 ( 𝑥 = 𝑦 → ( 𝑥𝑗 ) = ( 𝑦𝑗 ) )
2 1 oveq1d ( 𝑥 = 𝑦 → ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑦𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
3 2 cbvmptv ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( 𝑦𝑋 ↦ ( ( 𝑦𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
4 oveq2 ( 𝑗 = 𝑘 → ( 𝑦𝑗 ) = ( 𝑦𝑘 ) )
5 eqeq1 ( 𝑗 = 𝑘 → ( 𝑗 = 0 ↔ 𝑘 = 0 ) )
6 5 ifbid ( 𝑗 = 𝑘 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) = if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
7 4 6 oveq12d ( 𝑗 = 𝑘 → ( ( 𝑦𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑦𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
8 7 mpteq2dv ( 𝑗 = 𝑘 → ( 𝑦𝑋 ↦ ( ( 𝑦𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( 𝑦𝑋 ↦ ( ( 𝑦𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
9 3 8 syl5eq ( 𝑗 = 𝑘 → ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( 𝑦𝑋 ↦ ( ( 𝑦𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
10 9 cbvmptv ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥𝑋 ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦𝑋 ↦ ( ( 𝑦𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )