Theorem ovresd

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

	Ref	Expression
Hypotheses	ovresd.1	|- ( ph -> A e. X )
	ovresd.2	|- ( ph -> B e. X )
Assertion	ovresd	|- ( ph -> ( A ( D |` ( X X. X ) ) B ) = ( A D B ) )

Proof

Step	Hyp	Ref	Expression
1		ovresd.1	|- ( ph -> A e. X )
2		ovresd.2	|- ( ph -> B e. X )
3		ovres	|- ( ( A e. X /\ B e. X ) -> ( A ( D |` ( X X. X ) ) B ) = ( A D B ) )
4	1 2 3	syl2anc	|- ( ph -> ( A ( D |` ( X X. X ) ) B ) = ( A D B ) )