Metamath Proof Explorer


Theorem 0nei

Description: The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006)

Ref Expression
Assertion 0nei JTopneiJ

Proof

Step Hyp Ref Expression
1 0opn JTopJ
2 opnneiid JTopneiJJ
3 1 2 mpbird JTopneiJ