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	|- F/ x ph
	mpteq1df.2	|- ( ph -> A = B )
Assertion	mpteq1df	|- ( ph -> ( x e. A |-> C ) = ( x e. B |-> C ) )

Proof

Step	Hyp	Ref	Expression
1		mpteq1df.1	|- F/ x ph
2		mpteq1df.2	|- ( ph -> A = B )
3		eqidd	|- ( ph -> C = C )
4	1 2 3	mpteq12df	|- ( ph -> ( x e. A |-> C ) = ( x e. B |-> C ) )