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 } ) )