Theorem usgreqdrusgr

Description: If all vertices in a simple graph have the same degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020)

	Ref	Expression
Hypotheses	isrusgr0.v	|- V = ( Vtx ` G )
	isrusgr0.d	|- D = ( VtxDeg ` G )
Assertion	usgreqdrusgr	|- ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) -> G RegUSGraph K )

Proof

Step	Hyp	Ref	Expression
1		isrusgr0.v	|- V = ( Vtx ` G )
2		isrusgr0.d	|- D = ( VtxDeg ` G )
3	1 2	isrusgr0	|- ( ( G e. USGraph /\ K e. NN0* ) -> ( G RegUSGraph K <-> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) )
4	3	3adant3	|- ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) -> ( G RegUSGraph K <-> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) )
5	4	ibir	|- ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) -> G RegUSGraph K )