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	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge A\in X\right)\to ADA=0$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢A=A$$
2		xmeteq0	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge A\in X\wedge A\in X\right)\to \left(ADA=0\leftrightarrow A=A\right)$$
3	2	3anidm23	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge A\in X\right)\to \left(ADA=0\leftrightarrow A=A\right)$$
4	1 3	mpbiri	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge A\in X\right)\to ADA=0$$