Metamath Proof Explorer


Theorem iscld3

Description: A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006)

Ref Expression
Hypothesis clscld.1 X = J
Assertion iscld3 J Top S X S Clsd J cls J S = S

Proof

Step Hyp Ref Expression
1 clscld.1 X = J
2 cldcls S Clsd J cls J S = S
3 1 clscld J Top S X cls J S Clsd J
4 eleq1 cls J S = S cls J S Clsd J S Clsd J
5 3 4 syl5ibcom J Top S X cls J S = S S Clsd J
6 2 5 impbid2 J Top S X S Clsd J cls J S = S