This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovresd

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

Ref Expression
Hypotheses ovresd.1 ⊢ φ → A ∈ X
ovresd.2 ⊢ φ → B ∈ X
Assertion ovresd ⊢ φ → A D ↾ X × X B = A D B

Proof

Step Hyp Ref Expression
1 ovresd.1 ⊢ φ → A ∈ X
2 ovresd.2 ⊢ φ → B ∈ X
3 ovres ⊢ A ∈ X ∧ B ∈ X → A D ↾ X × X B = A D B
4 1 2 3 syl2anc ⊢ φ → A D ↾ X × X B = A D B