Theorem mpteq1df

Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021) (Proof shortened by SN, 11-Nov-2024)

	Ref	Expression
Hypotheses	mpteq1df.1	$$⊢Ⅎx\phi$$
	mpteq1df.2	$$⊢\phi \to A=B$$
Assertion	mpteq1df	$$⊢\phi \to \left(x\in A⟼C\right)=\left(x\in B⟼C\right)$$

Proof

Step	Hyp	Ref	Expression
1		mpteq1df.1	$$⊢Ⅎx\phi$$
2		mpteq1df.2	$$⊢\phi \to A=B$$
3		eqidd	$$⊢\phi \to C=C$$
4	1 2 3	mpteq12df	$$⊢\phi \to \left(x\in A⟼C\right)=\left(x\in B⟼C\right)$$