Step |
Hyp |
Ref |
Expression |
1 |
|
id |
|- ( v = X -> v = X ) |
2 |
|
oveq2 |
|- ( v = X -> ( G NeighbVtx v ) = ( G NeighbVtx X ) ) |
3 |
1 2
|
neleq12d |
|- ( v = X -> ( v e/ ( G NeighbVtx v ) <-> X e/ ( G NeighbVtx X ) ) ) |
4 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
5 |
4
|
nbgrnself |
|- A. v e. ( Vtx ` G ) v e/ ( G NeighbVtx v ) |
6 |
3 5
|
vtoclri |
|- ( X e. ( Vtx ` G ) -> X e/ ( G NeighbVtx X ) ) |
7 |
4
|
nbgrisvtx |
|- ( X e. ( G NeighbVtx X ) -> X e. ( Vtx ` G ) ) |
8 |
7
|
con3i |
|- ( -. X e. ( Vtx ` G ) -> -. X e. ( G NeighbVtx X ) ) |
9 |
|
df-nel |
|- ( X e/ ( G NeighbVtx X ) <-> -. X e. ( G NeighbVtx X ) ) |
10 |
8 9
|
sylibr |
|- ( -. X e. ( Vtx ` G ) -> X e/ ( G NeighbVtx X ) ) |
11 |
6 10
|
pm2.61i |
|- X e/ ( G NeighbVtx X ) |