Theorem met0

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 NM, 30-Aug-2006)

	Ref	Expression
Assertion	met0	|- ( ( D e. ( Met ` X ) /\ A e. X ) -> ( A D A ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		metxmet	|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
2		xmet0	|- ( ( D e. ( *Met ` X ) /\ A e. X ) -> ( A D A ) = 0 )
3	1 2	sylan	|- ( ( D e. ( Met ` X ) /\ A e. X ) -> ( A D A ) = 0 )