Metamath Proof Explorer


Theorem hashnbusgrvd

Description: In a simple graph, the number of neighbors of a vertex is the degree of this vertex. This theorem does not hold for (simple) pseudographs, because a vertex connected with itself only by a loop has no neighbors, see uspgrloopnb0 , but degree 2, see uspgrloopvd2 . And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 , but also degree 2, see umgr2v2evd2 . (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 15-Dec-2020) (Proof shortened by AV, 5-May-2021)

Ref Expression
Hypothesis hashnbusgrvd.v V = Vtx G
Assertion hashnbusgrvd G USGraph U V G NeighbVtx U = VtxDeg G U

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v V = Vtx G
2 eqid Edg G = Edg G
3 1 2 nbedgusgr G USGraph U V G NeighbVtx U = e Edg G | U e
4 eqid VtxDeg G = VtxDeg G
5 1 2 4 vtxdusgrfvedg G USGraph U V VtxDeg G U = e Edg G | U e
6 3 5 eqtr4d G USGraph U V G NeighbVtx U = VtxDeg G U