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	$$⊢\phi \to C=D$$
Assertion	mpoeq3dv	$$⊢\phi \to \left(x\in A,y\in B⟼C\right)=\left(x\in A,y\in B⟼D\right)$$

Proof

Step	Hyp	Ref	Expression
1		mpoeq3dv.1	$$⊢\phi \to C=D$$
2	1	3ad2ant1	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to C=D$$
3	2	mpoeq3dva	$$⊢\phi \to \left(x\in A,y\in B⟼C\right)=\left(x\in A,y\in B⟼D\right)$$