Theorem mpoeq3dv

Description: An equality deduction for the maps-to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018)

	Ref	Expression
Hypothesis	mpoeq3dv.1	|- ( ph -> C = D )
Assertion	mpoeq3dv	|- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )

Proof

Step	Hyp	Ref	Expression
1		mpoeq3dv.1	|- ( ph -> C = D )
2	1	3ad2ant1	|- ( ( ph /\ x e. A /\ y e. B ) -> C = D )
3	2	mpoeq3dva	|- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )