Metamath Proof Explorer

Theorem meteq0

Description: The value of a metric is zero iff its arguments are equal. Property M2 of Kreyszig p. 4. (Contributed by NM, 30-Aug-2006)

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

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

Step

Hyp

Ref

Expression

 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )

 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> A = B ) )

1 2

 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> A = B ) )