Theorem mpteq2ia

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013)

	Ref	Expression
Hypothesis	mpteq2ia.1	|- ( x e. A -> B = C )
Assertion	mpteq2ia	|- ( x e. A |-> B ) = ( x e. A |-> C )

Proof

Step	Hyp	Ref	Expression
1		mpteq2ia.1	|- ( x e. A -> B = C )
2		eqid	|- A = A
3	2	ax-gen	|- A. x A = A
4	1	rgen	|- A. x e. A B = C
5		mpteq12f	|- ( ( A. x A = A /\ A. x e. A B = C ) -> ( x e. A |-> B ) = ( x e. A |-> C ) )
6	3 4 5	mp2an	|- ( x e. A |-> B ) = ( x e. A |-> C )