Metamath Proof Explorer

Theorem metxmet

Description: A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion metxmet 
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )

Proof

Step Hyp Ref Expression
1 ismet2 
 |-  ( D e. ( Met ` X ) <-> ( D e. ( *Met ` X ) /\ D : ( X X. X ) --> RR ) )
2 1 simplbi 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )