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

Metamath Proof Explorer

Theorem mpteq1i

Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020) Remove all disjoint variable conditions. (Revised by SN, 11-Nov-2024)

		Ref	Expression
	Hypothesis	mpteq1i.1	⊢ 𝐴 = 𝐵
	Assertion	mpteq1i	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mpteq1i.1	⊢ 𝐴 = 𝐵
2	1	a1i	⊢ ( ⊤ → 𝐴 = 𝐵 )
3		eqidd	⊢ ( ⊤ → 𝐶 = 𝐶 )
4	2 3	mpteq12dv	⊢ ( ⊤ → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )
5	4	mptru	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )