Definition df-t1

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ct1	|- Fre
1		vx	|- x
2		ctop	|- Top
3		va	|- a
4	1	cv	|- x
5	4	cuni	|- U. x
6	3	cv	|- a
7	6	csn	|- { a }
8		ccld	|- Clsd
9	4 8	cfv	|- ( Clsd ` x )
10	7 9	wcel	|- { a } e. ( Clsd ` x )
11	10 3 5	wral	|- A. a e. U. x { a } e. ( Clsd ` x )
12	11 1 2	crab	|- { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) }
13	0 12	wceq	|- Fre = { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) }