This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0nei

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

Ref Expression
Assertion 0nei ⊢ J ∈ Top → ∅ ∈ nei ⁡ J ⁡ ∅

Proof

Step Hyp Ref Expression
1 0opn ⊢ J ∈ Top → ∅ ∈ J
2 opnneiid ⊢ J ∈ Top → ∅ ∈ nei ⁡ J ⁡ ∅ ↔ ∅ ∈ J
3 1 2 mpbird ⊢ J ∈ Top → ∅ ∈ nei ⁡ J ⁡ ∅