Metamath Proof Explorer


Theorem isopn3i

Description: An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Assertion isopn3i JTopSJintJS=S

Proof

Step Hyp Ref Expression
1 simpr JTopSJSJ
2 elssuni SJSJ
3 eqid J=J
4 3 isopn3 JTopSJSJintJS=S
5 2 4 sylan2 JTopSJSJintJS=S
6 1 5 mpbid JTopSJintJS=S