Metamath Proof Explorer

Theorem metdmdm

Description: Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion metdmdm 
|- ( D e. ( Met ` X ) -> X = dom dom D )

Proof

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