Theorem mpteq1df

Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	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	1 2	alrimi	|- ( ph -> A. x A = B )
4		eqid	|- C = C
5	4	rgenw	|- A. x e. A C = C
6		mpteq12f	|- ( ( A. x A = B /\ A. x e. A C = C ) -> ( x e. A |-> C ) = ( x e. B |-> C ) )
7	3 5 6	sylancl	|- ( ph -> ( x e. A |-> C ) = ( x e. B |-> C ) )