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

Metamath Proof Explorer

Theorem xmet0

Description: The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of Gleason p. 223. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmet0 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X → A D A = 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ A = A
2 xmeteq0 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ A ∈ X → A D A = 0 ↔ A = A
3 2 3anidm23 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X → A D A = 0 ↔ A = A
4 1 3 mpbiri ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X → A D A = 0