Theorem vtxdusgrval

Description: The value of the vertex degree function for a simple graph. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 11-Dec-2020)

	Ref	Expression
Hypotheses	vtxdlfgrval.v	|- V = ( Vtx ` G )
	vtxdlfgrval.i	|- I = ( iEdg ` G )
	vtxdlfgrval.a	|- A = dom I
	vtxdlfgrval.d	|- D = ( VtxDeg ` G )
Assertion	vtxdusgrval	|- ( ( G e. USGraph /\ U e. V ) -> ( D ` U ) = ( # ` { x e. A | U e. ( I ` x ) } ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdlfgrval.v	|- V = ( Vtx ` G )
2		vtxdlfgrval.i	|- I = ( iEdg ` G )
3		vtxdlfgrval.a	|- A = dom I
4		vtxdlfgrval.d	|- D = ( VtxDeg ` G )
5		usgrumgr	|- ( G e. USGraph -> G e. UMGraph )
6	1 2 3 4	vtxdumgrval	|- ( ( G e. UMGraph /\ U e. V ) -> ( D ` U ) = ( # ` { x e. A | U e. ( I ` x ) } ) )
7	5 6	sylan	|- ( ( G e. USGraph /\ U e. V ) -> ( D ` U ) = ( # ` { x e. A | U e. ( I ` x ) } ) )