Theorem mpoeq123dv

Description: An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011)

	Ref	Expression
Hypotheses	mpoeq123dv.1	|- ( ph -> A = D )
	mpoeq123dv.2	|- ( ph -> B = E )
	mpoeq123dv.3	|- ( ph -> C = F )
Assertion	mpoeq123dv	|- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )

Proof

Step	Hyp	Ref	Expression
1		mpoeq123dv.1	|- ( ph -> A = D )
2		mpoeq123dv.2	|- ( ph -> B = E )
3		mpoeq123dv.3	|- ( ph -> C = F )
4	2	adantr	|- ( ( ph /\ x e. A ) -> B = E )
5	3	adantr	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = F )
6	1 4 5	mpoeq123dva	|- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )