Metamath Proof Explorer


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 G NeighbVtx X X V

Proof

Step Hyp Ref Expression
1 nbgrcl.v V = Vtx G
2 df-nbgr NeighbVtx = g V , v Vtx g n Vtx g v | e Edg g v n e
3 2 mpoxeldm N G NeighbVtx X G V X 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 G / g Vtx g X V
7 6 biimpi X G / g Vtx g X V
8 3 7 simpl2im N G NeighbVtx X X V