Theorem nbgrnvtx0

Description: If a class X is not a vertex of a graph G , then it has no neighbors in G . (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020)

	Ref	Expression
Hypothesis	nbgrel.v	|- V = ( Vtx ` G )
Assertion	nbgrnvtx0	|- ( X e/ V -> ( G NeighbVtx X ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		nbgrel.v	|- V = ( Vtx ` G )
2		csbfv	|- [_ G / g ]_ ( Vtx ` g ) = ( Vtx ` G )
3	1 2	eqtr4i	|- V = [_ G / g ]_ ( Vtx ` g )
4		neleq2	|- ( V = [_ G / g ]_ ( Vtx ` g ) -> ( X e/ V <-> X e/ [_ G / g ]_ ( Vtx ` g ) ) )
5	3 4	ax-mp	|- ( X e/ V <-> X e/ [_ G / g ]_ ( Vtx ` g ) )
6	5	biimpi	|- ( X e/ V -> X e/ [_ G / g ]_ ( Vtx ` g ) )
7	6	olcd	|- ( X e/ V -> ( G e/ _V \/ X e/ [_ G / g ]_ ( Vtx ` g ) ) )
8		df-nbgr	|- NeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> { n e. ( ( Vtx ` g ) \ { v } ) | E. e e. ( Edg ` g ) { v , n } C_ e } )
9	8	mpoxneldm	|- ( ( G e/ _V \/ X e/ [_ G / g ]_ ( Vtx ` g ) ) -> ( G NeighbVtx X ) = (/) )
10	7 9	syl	|- ( X e/ V -> ( G NeighbVtx X ) = (/) )