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 e. ( *Met ` X ) /\ A e. X ) -> ( A D A ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- A = A
2		xmeteq0	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ A e. X ) -> ( ( A D A ) = 0 <-> A = A ) )
3	2	3anidm23	|- ( ( D e. ( *Met ` X ) /\ A e. X ) -> ( ( A D A ) = 0 <-> A = A ) )
4	1 3	mpbiri	|- ( ( D e. ( *Met ` X ) /\ A e. X ) -> ( A D A ) = 0 )