Theorem vtxdusgr0edgnel

Description: A vertex in a simple graph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020) (Proof shortened by AV, 24-Dec-2020)

	Ref	Expression
Hypotheses	vtxdushgrfvedg.v	|- V = ( Vtx ` G )
	vtxdushgrfvedg.e	|- E = ( Edg ` G )
	vtxdushgrfvedg.d	|- D = ( VtxDeg ` G )
Assertion	vtxdusgr0edgnel	|- ( ( G e. USGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. e e. E U e. e ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdushgrfvedg.v	|- V = ( Vtx ` G )
2		vtxdushgrfvedg.e	|- E = ( Edg ` G )
3		vtxdushgrfvedg.d	|- D = ( VtxDeg ` G )
4		usgruhgr	|- ( G e. USGraph -> G e. UHGraph )
5	1 2 3	vtxduhgr0edgnel	|- ( ( G e. UHGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. e e. E U e. e ) )
6	4 5	sylan	|- ( ( G e. USGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. e e. E U e. e ) )