Metamath Proof Explorer

Theorem meteq0

Description: The value of a metric is zero iff its arguments are equal. Property M2 of Kreyszig p. 4. (Contributed by NM, 30-Aug-2006)

Ref Expression
Assertion meteq0 ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = 0 ↔ A = B

Proof

Step Hyp Ref Expression
1 metxmet ⊢ D ∈ Met ⁡ X → D ∈ ∞Met ⁡ X
2 xmeteq0 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = 0 ↔ A = B
3 1 2 syl3an1 ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = 0 ↔ A = B