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∞MetXAXADA=0

Proof

Step Hyp Ref Expression
1 eqid A=A
2 xmeteq0 D∞MetXAXAXADA=0A=A
3 2 3anidm23 D∞MetXAXADA=0A=A
4 1 3 mpbiri D∞MetXAXADA=0