Theorem cmetmeti

Description: A complete metric space is a metric space. (Contributed by NM, 26-Oct-2007)

	Ref	Expression
Hypothesis	cmetmeti.1	|- D e. ( CMet ` X )
Assertion	cmetmeti	|- D e. ( Met ` X )

Proof

Step	Hyp	Ref	Expression
1		cmetmeti.1	|- D e. ( CMet ` X )
2		cmetmet	|- ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
3	1 2	ax-mp	|- D e. ( Met ` X )