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 ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 𝐷 𝐡 ) = 0 ↔ 𝐴 = 𝐡 ) )

Proof

Step Hyp Ref Expression
1 metxmet ⊒ ( 𝐷 ∈ ( Met β€˜ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
2 xmeteq0 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 𝐷 𝐡 ) = 0 ↔ 𝐴 = 𝐡 ) )
3 1 2 syl3an1 ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( ( 𝐴 𝐷 𝐡 ) = 0 ↔ 𝐴 = 𝐡 ) )