Theorem nbgrcl

Description: If a class X has at least one neighbor, this class must be a vertex. (Contributed by AV, 6-Jun-2021) (Revised by AV, 12-Feb-2022)

	Ref	Expression
Hypothesis	nbgrcl.v	|- V = ( Vtx ` G )
Assertion	nbgrcl	|- ( N e. ( G NeighbVtx X ) -> X e. V )

Proof

Step	Hyp	Ref	Expression
1		nbgrcl.v	|- V = ( Vtx ` G )
2		df-nbgr	|- NeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> { n e. ( ( Vtx ` g ) \ { v } ) | E. e e. ( Edg ` g ) { v , n } C_ e } )
3	2	mpoxeldm	|- ( N e. ( G NeighbVtx X ) -> ( G e. _V /\ X e. [_ G / g ]_ ( Vtx ` g ) ) )
4		csbfv	|- [_ G / g ]_ ( Vtx ` g ) = ( Vtx ` G )
5	4 1	eqtr4i	|- [_ G / g ]_ ( Vtx ` g ) = V
6	5	eleq2i	|- ( X e. [_ G / g ]_ ( Vtx ` g ) <-> X e. V )
7	6	biimpi	|- ( X e. [_ G / g ]_ ( Vtx ` g ) -> X e. V )
8	3 7	simpl2im	|- ( N e. ( G NeighbVtx X ) -> X e. V )