Theorem mpteq2da

Description: Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013) (Revised by Mario Carneiro, 16-Dec-2013)

	Ref	Expression
Hypotheses	mpteq2da.1	|- F/ x ph
	mpteq2da.2	|- ( ( ph /\ x e. A ) -> B = C )
Assertion	mpteq2da	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Proof

Step	Hyp	Ref	Expression
1		mpteq2da.1	|- F/ x ph
2		mpteq2da.2	|- ( ( ph /\ x e. A ) -> B = C )
3		eqid	|- A = A
4	3	ax-gen	|- A. x A = A
5	2	ex	|- ( ph -> ( x e. A -> B = C ) )
6	1 5	ralrimi	|- ( ph -> A. x e. A B = C )
7		mpteq12f	|- ( ( A. x A = A /\ A. x e. A B = C ) -> ( x e. A |-> B ) = ( x e. A |-> C ) )
8	4 6 7	sylancr	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )