Description: If a class X is not a vertex of a graph G , then it has no neighbors in G . (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nbgrel.v | |
|
Assertion | nbgrnvtx0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nbgrel.v | |
|
2 | csbfv | |
|
3 | 1 2 | eqtr4i | |
4 | neleq2 | |
|
5 | 3 4 | ax-mp | |
6 | 5 | biimpi | |
7 | 6 | olcd | |
8 | df-nbgr | |
|
9 | 8 | mpoxneldm | |
10 | 7 9 | syl | |