Theorem cbvmpov

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt , some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013)

	Ref	Expression
Hypotheses	cbvmpov.1	⊢ ( 𝑥 = 𝑧 → 𝐶 = 𝐸 )
	cbvmpov.2	⊢ ( 𝑦 = 𝑤 → 𝐸 = 𝐷 )
Assertion	cbvmpov	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐵 ↦ 𝐷 )

Proof

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