Theorem mpteq12dva

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		mpteq12dv.1	|- ( ph -> A = C )
2		mpteq12dva.2	|- ( ( ph /\ x e. A ) -> B = D )
3	1	alrimiv	|- ( ph -> A. x A = C )
4	2	ralrimiva	|- ( ph -> A. x e. A B = D )
5		mpteq12f	|- ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
6	3 4 5	syl2anc	|- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )