This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )