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
|- X e/ ( G NeighbVtx X )

Proof

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 )