# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}\left\{{a}\right\}\in \mathrm{Clsd}\left({x}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ct1 ${class}\mathrm{Fre}$
1 vx ${setvar}{x}$
2 ctop ${class}\mathrm{Top}$
3 va ${setvar}{a}$
4 1 cv ${setvar}{x}$
5 4 cuni ${class}\bigcup {x}$
6 3 cv ${setvar}{a}$
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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\left\{{a}\right\}\in \mathrm{Clsd}\left({x}\right)\right\}$