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 = { 𝑥 ∈ Top ∣ ∀ 𝑎 ∈ ∪ 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ct1	⊢ Fre
1		vx	⊢ 𝑥
2		ctop	⊢ Top
3		va	⊢ 𝑎
4	1	cv	⊢ 𝑥
5	4	cuni	⊢ ∪ 𝑥
6	3	cv	⊢ 𝑎
7	6	csn	⊢ { 𝑎 }
8		ccld	⊢ Clsd
9	4 8	cfv	⊢ ( Clsd ‘ 𝑥 )
10	7 9	wcel	⊢ { 𝑎 } ∈ ( Clsd ‘ 𝑥 )
11	10 3 5	wral	⊢ ∀ 𝑎 ∈ ∪ 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 )
12	11 1 2	crab	⊢ { 𝑥 ∈ Top ∣ ∀ 𝑎 ∈ ∪ 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) }
13	0 12	wceq	⊢ Fre = { 𝑥 ∈ Top ∣ ∀ 𝑎 ∈ ∪ 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) }