Theorem mpoeq123i

Description: An equality inference for the maps-to notation. (Contributed by NM, 15-Jul-2013)

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

Proof

Step	Hyp	Ref	Expression
1		mpoeq123i.1	⊢ 𝐴 = 𝐷
2		mpoeq123i.2	⊢ 𝐵 = 𝐸
3		mpoeq123i.3	⊢ 𝐶 = 𝐹
4	1	a1i	⊢ ( ⊤ → 𝐴 = 𝐷 )
5	2	a1i	⊢ ( ⊤ → 𝐵 = 𝐸 )
6	3	a1i	⊢ ( ⊤ → 𝐶 = 𝐹 )
7	4 5 6	mpoeq123dv	⊢ ( ⊤ → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ 𝐸 ↦ 𝐹 ) )
8	7	mptru	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ 𝐸 ↦ 𝐹 )