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

Metamath Proof Explorer

Theorem mpoeq123dva

Description: An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		mpoeq123dv.1	⊢ ( 𝜑 → 𝐴 = 𝐷 )
2		mpoeq123dva.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐸 )
3		mpoeq123dva.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 = 𝐹 )
4	3	eqeq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐹 ) )
5	4	pm5.32da	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐹 ) ) )
6	2	eleq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐸 ) )
7	6	pm5.32da	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐸 ) ) )
8	1	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐷 ) )
9	8	anbi1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐸 ) ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) ) )
10	7 9	bitrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) ) )
11	10	anbi1d	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐹 ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 = 𝐹 ) ) )
12	5 11	bitrd	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 = 𝐹 ) ) )
13	12	oprabbidv	⊢ ( 𝜑 → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 = 𝐹 ) } )
14		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
15		df-mpo	⊢ ( 𝑥 ∈ 𝐷 , 𝑦 ∈ 𝐸 ↦ 𝐹 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 = 𝐹 ) }
16	13 14 15	3eqtr4g	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ 𝐸 ↦ 𝐹 ) )