Step 
Hyp 
Ref 
Expression 
1 

eqid 
⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 
2 
1

fvmpt2i 
⊢ ( 𝑘 ∈ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = ( I ‘ 𝐵 ) ) 
3 
2

prodeq2i 
⊢ ∏ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = ∏ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) 
4 

nffvmpt1 
⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) 
5 

nfcv 
⊢ Ⅎ 𝑗 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) 
6 

fveq2 
⊢ ( 𝑗 = 𝑘 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) 
7 
4 5 6

cbvprodi 
⊢ ∏ 𝑗 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ∏ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) 
8 

prod2id 
⊢ ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) 
9 
3 7 8

3eqtr4i 
⊢ ∏ 𝑗 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ∏ 𝑘 ∈ 𝐴 𝐵 