Theorem sncld

Description: A singleton is closed in a Hausdorff space. (Contributed by NM, 5-Mar-2007) (Revised by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Hypothesis	t1sep.1	|- X = U. J
Assertion	sncld	|- ( ( J e. Haus /\ P e. X ) -> { P } e. ( Clsd ` J ) )

Proof

Step	Hyp	Ref	Expression
1		t1sep.1	|- X = U. J
2		haust1	|- ( J e. Haus -> J e. Fre )
3	1	t1sncld	|- ( ( J e. Fre /\ P e. X ) -> { P } e. ( Clsd ` J ) )
4	2 3	sylan	|- ( ( J e. Haus /\ P e. X ) -> { P } e. ( Clsd ` J ) )