Metamath Proof Explorer


Theorem opnneiid

Description: Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006)

Ref Expression
Assertion opnneiid J Top N nei J N N J

Proof

Step Hyp Ref Expression
1 neii2 J Top N nei J N x J N x x N
2 eqss N = x N x x N
3 eleq1a x J N = x N J
4 2 3 syl5bir x J N x x N N J
5 4 rexlimiv x J N x x N N J
6 1 5 syl J Top N nei J N N J
7 6 ex J Top N nei J N N J
8 ssid N N
9 opnneiss J Top N J N N N nei J N
10 9 3exp J Top N J N N N nei J N
11 8 10 mpii J Top N J N nei J N
12 7 11 impbid J Top N nei J N N J