Metamath Proof Explorer


Theorem nbgrnself2

Description: A class X is not a neighbor of itself (whether it is a vertex or not). (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 3-Nov-2020) (Revised by AV, 12-Feb-2022)

Ref Expression
Assertion nbgrnself2 XGNeighbVtxX

Proof

Step Hyp Ref Expression
1 id v=Xv=X
2 oveq2 v=XGNeighbVtxv=GNeighbVtxX
3 1 2 neleq12d v=XvGNeighbVtxvXGNeighbVtxX
4 eqid VtxG=VtxG
5 4 nbgrnself vVtxGvGNeighbVtxv
6 3 5 vtoclri XVtxGXGNeighbVtxX
7 4 nbgrisvtx XGNeighbVtxXXVtxG
8 7 con3i ¬XVtxG¬XGNeighbVtxX
9 df-nel XGNeighbVtxX¬XGNeighbVtxX
10 8 9 sylibr ¬XVtxGXGNeighbVtxX
11 6 10 pm2.61i XGNeighbVtxX