Metamath Proof Explorer


Theorem nbgrisvtx

Description: Every neighbor N of a vertex K is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020) (Revised by AV, 12-Feb-2022)

Ref Expression
Hypothesis nbgrisvtx.v V = Vtx G
Assertion nbgrisvtx N G NeighbVtx K N V

Proof

Step Hyp Ref Expression
1 nbgrisvtx.v V = Vtx G
2 eqid Edg G = Edg G
3 1 2 nbgrel N G NeighbVtx K N V K V N K e Edg G K N e
4 simp1l N V K V N K e Edg G K N e N V
5 3 4 sylbi N G NeighbVtx K N V