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	$$⊢\mathrm{Fre}=\left\{x\in \mathrm{Top}|\forall a\in \bigcup x\left\{a\right\}\in \mathrm{Clsd}\left(x\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ct1	$$class\mathrm{Fre}$$
1		vx	$$setvarx$$
2		ctop	$$class\mathrm{Top}$$
3		va	$$setvara$$
4	1	cv	$$setvarx$$
5	4	cuni	$$class\bigcup x$$
6	3	cv	$$setvara$$
7	6	csn	$$class\left\{a\right\}$$
8		ccld	$$class\mathrm{Clsd}$$
9	4 8	cfv	$$class\mathrm{Clsd}\left(x\right)$$
10	7 9	wcel	$$wff\left\{a\right\}\in \mathrm{Clsd}\left(x\right)$$
11	10 3 5	wral	$$wff\forall a\in \bigcup x\left\{a\right\}\in \mathrm{Clsd}\left(x\right)$$
12	11 1 2	crab	$$class\left\{x\in \mathrm{Top}|\forall a\in \bigcup x\left\{a\right\}\in \mathrm{Clsd}\left(x\right)\right\}$$
13	0 12	wceq	$$wff\mathrm{Fre}=\left\{x\in \mathrm{Top}|\forall a\in \bigcup x\left\{a\right\}\in \mathrm{Clsd}\left(x\right)\right\}$$