Theorem ovresd

Description: Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	ovresd.1	$$⊢\phi \to A\in X$$
	ovresd.2	$$⊢\phi \to B\in X$$
Assertion	ovresd	$$⊢\phi \to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B=ADB$$

Proof

Step	Hyp	Ref	Expression
1		ovresd.1	$$⊢\phi \to A\in X$$
2		ovresd.2	$$⊢\phi \to B\in X$$
3		ovres	$$⊢\left(A\in X\wedge B\in X\right)\to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B=ADB$$
4	1 2 3	syl2anc	$$⊢\phi \to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B=ADB$$