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 \in Top \land N \in J \land P \in N) \to N \in nei (J) (\{P\})$

Step	Hyp	Ref	Expression
1		snssi	$⊢ P \in N \to \{P\} \subseteq N$
2		opnneiss	$⊢ (J \in Top \land N \in J \land \{P\} \subseteq N) \to N \in nei (J) (\{P\})$
3	1 2	syl3an3	$⊢ (J \in Top \land N \in J \land P \in N) \to N \in nei (J) (\{P\})$