Metamath Proof Explorer

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 φ C = D
Assertion mpoeq3dv φ x A , y B C = x A , y B D


Step Hyp Ref Expression
1 mpoeq3dv.1 φ C = D
2 1 3ad2ant1 φ x A y B C = D
3 2 mpoeq3dva φ x A , y B C = x A , y B D