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

Metamath Proof Explorer

Theorem mpteq12

Description: An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013)

		Ref	Expression
	Assertion	mpteq12	⊢ ( ( 𝐴 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) )

Step	Hyp	Ref	Expression
1		ax-5	⊢ ( 𝐴 = 𝐶 → ∀ 𝑥 𝐴 = 𝐶 )
2		mpteq12f	⊢ ( ( ∀ 𝑥 𝐴 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) )
3	1 2	sylan	⊢ ( ( 𝐴 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) )