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	$⊢ A = B$
	Assertion	mpteq1i	$⊢ (x \in A ⟼ C) = (x \in B ⟼ C)$

Proof

Step	Hyp	Ref	Expression
1		mpteq1i.1	$⊢ A = B$
2	1	a1i	$⊢ ⊤ \to A = B$
3		eqidd	$⊢ ⊤ \to C = C$
4	2 3	mpteq12dv	$⊢ ⊤ \to (x \in A ⟼ C) = (x \in B ⟼ C)$
5	4	mptru	$⊢ (x \in A ⟼ C) = (x \in B ⟼ C)$