Description: Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | opnneiid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neii2 | |
|
2 | eqss | |
|
3 | eleq1a | |
|
4 | 2 3 | syl5bir | |
5 | 4 | rexlimiv | |
6 | 1 5 | syl | |
7 | 6 | ex | |
8 | ssid | |
|
9 | opnneiss | |
|
10 | 9 | 3exp | |
11 | 8 10 | mpii | |
12 | 7 11 | impbid | |