Theorem cmetmeti

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

	Ref	Expression
Hypothesis	cmetmeti.1	$$⊢D\in \mathrm{CMet}\left(X\right)$$
Assertion	cmetmeti	$$⊢D\in \mathrm{Met}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		cmetmeti.1	$$⊢D\in \mathrm{CMet}\left(X\right)$$
2		cmetmet	$$⊢D\in \mathrm{CMet}\left(X\right)\to D\in \mathrm{Met}\left(X\right)$$
3	1 2	ax-mp	$$⊢D\in \mathrm{Met}\left(X\right)$$