Metamath Proof Explorer

Theorem metpsmet

Description: A metric is a pseudometric. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion metpsmet 
|- ( D e. ( Met ` X ) -> D e. ( PsMet ` X ) )

Proof

Step Hyp Ref Expression
1 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
2 xmetpsmet 
 |-  ( D e. ( *Met ` X ) -> D e. ( PsMet ` X ) )
3 1 2 syl 
 |-  ( D e. ( Met ` X ) -> D e. ( PsMet ` X ) )