Metamath Proof Explorer


Theorem clnbgrcl

Description: If a class X has at least one element in its closed neighborhood, this class must be a vertex. (Contributed by AV, 7-May-2025)

Ref Expression
Hypothesis clnbgrcl.v V = Vtx G
Assertion clnbgrcl N G ClNeighbVtx X X V

Proof

Step Hyp Ref Expression
1 clnbgrcl.v V = Vtx G
2 df-clnbgr ClNeighbVtx = g V , v Vtx g v n Vtx g | e Edg g v n e
3 2 mpoxeldm N G ClNeighbVtx 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 ClNeighbVtx X X V