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 e. Top -> (/) e. ( ( nei ` J ) ` (/) ) )

Proof

Step Hyp Ref Expression
1 0opn 
 |-  ( J e. Top -> (/) e. J )
2 opnneiid 
 |-  ( J e. Top -> ( (/) e. ( ( nei ` J ) ` (/) ) <-> (/) e. J ) )
3 1 2 mpbird 
 |-  ( J e. Top -> (/) e. ( ( nei ` J ) ` (/) ) )