Theorem nbgrssovtx

Description: The neighbors of a vertex X form a subset of all vertices except the vertex X itself. Stronger version of nbgrssvtx . (Contributed by Alexander van der Vekens, 13-Jul-2018) (Revised by AV, 3-Nov-2020) (Revised by AV, 12-Feb-2022)

	Ref	Expression
Hypothesis	nbgrssovtx.v	|- V = ( Vtx ` G )
Assertion	nbgrssovtx	|- ( G NeighbVtx X ) C_ ( V \ { X } )

Proof

Step	Hyp	Ref	Expression
1		nbgrssovtx.v	|- V = ( Vtx ` G )
2	1	nbgrisvtx	|- ( v e. ( G NeighbVtx X ) -> v e. V )
3		nbgrnself2	|- X e/ ( G NeighbVtx X )
4		df-nel	|- ( v e/ ( G NeighbVtx X ) <-> -. v e. ( G NeighbVtx X ) )
5		neleq1	|- ( v = X -> ( v e/ ( G NeighbVtx X ) <-> X e/ ( G NeighbVtx X ) ) )
6	4 5	bitr3id	|- ( v = X -> ( -. v e. ( G NeighbVtx X ) <-> X e/ ( G NeighbVtx X ) ) )
7	3 6	mpbiri	|- ( v = X -> -. v e. ( G NeighbVtx X ) )
8	7	necon2ai	|- ( v e. ( G NeighbVtx X ) -> v =/= X )
9		eldifsn	|- ( v e. ( V \ { X } ) <-> ( v e. V /\ v =/= X ) )
10	2 8 9	sylanbrc	|- ( v e. ( G NeighbVtx X ) -> v e. ( V \ { X } ) )
11	10	ssriv	|- ( G NeighbVtx X ) C_ ( V \ { X } )