Metamath Proof Explorer


Theorem clnbgrisvtx

Description: Every member N of the closed neighborhood of a vertex K is a vertex. (Contributed by AV, 9-May-2025)

Ref Expression
Hypothesis clnbgrvtxel.v V = Vtx G
Assertion clnbgrisvtx N G ClNeighbVtx K N V

Proof

Step Hyp Ref Expression
1 clnbgrvtxel.v V = Vtx G
2 eqid Edg G = Edg G
3 1 2 clnbgrel N G ClNeighbVtx K N V K V N = K e Edg G K N e
4 simpll N V K V N = K e Edg G K N e N V
5 3 4 sylbi N G ClNeighbVtx K N V