Theorem t1sncld

Description: In a T_1 space, singletons are closed. (Contributed by Jeff Hankins, 1-Feb-2010)

	Ref	Expression
Hypothesis	ist0.1	|- X = U. J
Assertion	t1sncld	|- ( ( J e. Fre /\ A e. X ) -> { A } e. ( Clsd ` J ) )

Proof

Step	Hyp	Ref	Expression
1		ist0.1	|- X = U. J
2	1	ist1	|- ( J e. Fre <-> ( J e. Top /\ A. x e. X { x } e. ( Clsd ` J ) ) )
3		sneq	|- ( x = A -> { x } = { A } )
4	3	eleq1d	|- ( x = A -> ( { x } e. ( Clsd ` J ) <-> { A } e. ( Clsd ` J ) ) )
5	4	rspccv	|- ( A. x e. X { x } e. ( Clsd ` J ) -> ( A e. X -> { A } e. ( Clsd ` J ) ) )
6	2 5	simplbiim	|- ( J e. Fre -> ( A e. X -> { A } e. ( Clsd ` J ) ) )
7	6	imp	|- ( ( J e. Fre /\ A e. X ) -> { A } e. ( Clsd ` J ) )