Metamath Proof Explorer

Theorem metsym

Description: The distance function of a metric space is symmetric. Definition 14-1.1(c) of Gleason p. 223. (Contributed by NM, 27-Aug-2006) (Revised by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion metsym ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = B D A

Proof

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