Theorem metdmdm 9085

Description: The base set of a metric space in terms of its distance function.

Hypothesis

Ref	Expression
metf.1	|- X = dom dom D

Assertion

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

Proof of Theorem metdmdm

Step	Hyp	Ref	Expression
1		metf.1	. 2 |- X = dom dom D
2	1	a1i 8	1 |- (D e. Met -> X = dom dom D)

Syntax hints:   -> wi 3   = wceq 1298   e. wcel 1300  dom cdm 3986  Metcme 9066

This theorem was proved from axioms:  ax-1 4  ax-mp 7

Copyright terms: Public domain