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	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐵 ↦ 𝐷 )