Theorem mpoeq123dv

Description: An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011)

	Ref	Expression
Hypotheses	mpoeq123dv.1	⊢ ( 𝜑 → 𝐴 = 𝐷 )
	mpoeq123dv.2	⊢ ( 𝜑 → 𝐵 = 𝐸 )
	mpoeq123dv.3	⊢ ( 𝜑 → 𝐶 = 𝐹 )
Assertion	mpoeq123dv	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ 𝐸 ↦ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		mpoeq123dv.1	⊢ ( 𝜑 → 𝐴 = 𝐷 )
2		mpoeq123dv.2	⊢ ( 𝜑 → 𝐵 = 𝐸 )
3		mpoeq123dv.3	⊢ ( 𝜑 → 𝐶 = 𝐹 )
4	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐸 )
5	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 = 𝐹 )
6	1 4 5	mpoeq123dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ 𝐸 ↦ 𝐹 ) )