This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvmpo

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013)

Ref Expression
Hypotheses cbvmpo.1 ⊢ Ⅎ 𝑧 𝐶
cbvmpo.2 ⊢ Ⅎ 𝑤 𝐶
cbvmpo.3 ⊢ Ⅎ 𝑥 𝐷
cbvmpo.4 ⊢ Ⅎ 𝑦 𝐷
cbvmpo.5 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝐶 = 𝐷 )
Assertion cbvmpo ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐵 ↦ 𝐷 )

Proof

Step Hyp Ref Expression
1 cbvmpo.1 ⊢ Ⅎ 𝑧 𝐶
2 cbvmpo.2 ⊢ Ⅎ 𝑤 𝐶
3 cbvmpo.3 ⊢ Ⅎ 𝑥 𝐷
4 cbvmpo.4 ⊢ Ⅎ 𝑦 𝐷
5 cbvmpo.5 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝐶 = 𝐷 )
6 nfcv ⊢ Ⅎ 𝑧 𝐵
7 nfcv ⊢ Ⅎ 𝑥 𝐵
8 eqidd ⊢ ( 𝑥 = 𝑧 → 𝐵 = 𝐵 )
9 6 7 1 2 3 4 8 5 cbvmpox ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐵 ↦ 𝐷 )