Metamath Proof Explorer


Theorem opnneip

Description: An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007)

Ref Expression
Assertion opnneip
|- ( ( J e. Top /\ N e. J /\ P e. N ) -> N e. ( ( nei ` J ) ` { P } ) )

Proof

Step Hyp Ref Expression
1 snssi
 |-  ( P e. N -> { P } C_ N )
2 opnneiss
 |-  ( ( J e. Top /\ N e. J /\ { P } C_ N ) -> N e. ( ( nei ` J ) ` { P } ) )
3 1 2 syl3an3
 |-  ( ( J e. Top /\ N e. J /\ P e. N ) -> N e. ( ( nei ` J ) ` { P } ) )