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 e. USGraph /\ U e. 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 e. USGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) = ( # ` { e e. ( Edg ` G ) | U e. e } ) )
4		eqid	|- ( VtxDeg ` G ) = ( VtxDeg ` G )
5	1 2 4	vtxdusgrfvedg	|- ( ( G e. USGraph /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( # ` { e e. ( Edg ` G ) | U e. e } ) )
6	3 5	eqtr4d	|- ( ( G e. USGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) = ( ( VtxDeg ` G ) ` U ) )