Theorem vtxdusgradjvtx

Description: The degree of a vertex in a simple graph is the number of vertices adjacent to this vertex. (Contributed by Alexander van der Vekens, 9-Jul-2018) (Revised by AV, 23-Dec-2020)

	Ref	Expression
Hypotheses	vtxdusgradjvtx.v	|- V = ( Vtx ` G )
	vtxdusgradjvtx.e	|- E = ( Edg ` G )
Assertion	vtxdusgradjvtx	|- ( ( G e. USGraph /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( # ` { v e. V | { U , v } e. E } ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdusgradjvtx.v	|- V = ( Vtx ` G )
2		vtxdusgradjvtx.e	|- E = ( Edg ` G )
3	1	hashnbusgrvd	|- ( ( G e. USGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) = ( ( VtxDeg ` G ) ` U ) )
4	1 2	nbusgrvtx	|- ( ( G e. USGraph /\ U e. V ) -> ( G NeighbVtx U ) = { v e. V | { U , v } e. E } )
5	4	fveq2d	|- ( ( G e. USGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) = ( # ` { v e. V | { U , v } e. E } ) )
6	3 5	eqtr3d	|- ( ( G e. USGraph /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( # ` { v e. V | { U , v } e. E } ) )