Definition df-t1 21118

Description: The class of all T₁ spaces, also called Fréchet spaces. Morris, Topology without tears, p. 30 ex. 3. (Contributed by FL, 18-Jun-2007.)

Assertion

Ref	Expression
df-t1	|- Fre = { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) }

Distinct variable group:   x, a

Detailed syntax breakdown of Definition df-t1

Step	Hyp	Ref	Expression
1		ct1 21111	. 2 class Fre
2		va	. . . . . . 7 setvar a
3	2	cv 1482	. . . . . 6 class a
4	3	csn 4177	. . . . 5 class { a }
5		vx	. . . . . . 7 setvar x
6	5	cv 1482	. . . . . 6 class x
7		ccld 20820	. . . . . 6 class Clsd
8	6, 7	cfv 5888	. . . . 5 class ( Clsd ` x )
9	4, 8	wcel 1990	. . . 4 wff { a } e. ( Clsd ` x )
10	6	cuni 4436	. . . 4 class U. x
11	9, 2, 10	wral 2912	. . 3 wff A. a e. U. x { a } e. ( Clsd ` x )
12		ctop 20698	. . 3 class Top
13	11, 5, 12	crab 2916	. 2 class { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) }
14	1, 13	wceq 1483	1 wff Fre = { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) }

This definition is referenced by:  ist1  21125