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 )