Theorem usgrvd00

Description: If every vertex in a simple graph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018) (Revised by AV, 17-Dec-2020) (Proof shortened by AV, 23-Dec-2020)

	Ref	Expression
Hypotheses	vtxdusgradjvtx.v	|- V = ( Vtx ` G )
	vtxdusgradjvtx.e	|- E = ( Edg ` G )
Assertion	usgrvd00	|- ( G e. USGraph -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = 0 -> E = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdusgradjvtx.v	|- V = ( Vtx ` G )
2		vtxdusgradjvtx.e	|- E = ( Edg ` G )
3		usgruhgr	|- ( G e. USGraph -> G e. UHGraph )
4	1 2	uhgrvd00	|- ( G e. UHGraph -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = 0 -> E = (/) ) )
5	3 4	syl	|- ( G e. USGraph -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = 0 -> E = (/) ) )