Definition df-ms 7794

Description: Define the (proper) class of all metric spaces.

Assertion

Ref	Expression
df-ms	|- MetSp = {<.x, y>. | (y e. Met /\ x = dom dom y)}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-ms

Step	Hyp	Ref	Expression
1		cmt 7790	. 2 class MetSp
2		vy	. . . . . 6 set y
3	2	cv 955	. . . . 5 class y
4		cme 7789	. . . . 5 class Met
5	3, 4	wcel 958	. . . 4 wff y e. Met
6		vx	. . . . . 6 set x
7	6	cv 955	. . . . 5 class x
8	3	cdm 3170	. . . . . 6 class dom y
9	8	cdm 3170	. . . . 5 class dom dom y
10	7, 9	wceq 956	. . . 4 wff x = dom dom y
11	5, 10	wa 223	. . 3 wff (y e. Met /\ x = dom dom y)
12	11, 6, 2	copab 2666	. 2 class {<.x, y>. | (y e. Met /\ x = dom dom y)}
13	1, 12	wceq 956	1 wff MetSp = {<.x, y>. | (y e. Met /\ x = dom dom y)}

This definition is referenced by:  msrel 7797  dfms2 7799

Copyright terms: Public domain