Theorem mpteq12

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

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

Proof

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