Theorem vtxdg0v

Description: The degree of a vertex in the null graph is zero (or anything else), because there are no vertices. (Contributed by AV, 11-Dec-2020)

	Ref	Expression
Hypothesis	vtxdgf.v	|- V = ( Vtx ` G )
Assertion	vtxdg0v	|- ( ( G = (/) /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		vtxdgf.v	|- V = ( Vtx ` G )
2	1	eleq2i	|- ( U e. V <-> U e. ( Vtx ` G ) )
3		fveq2	|- ( G = (/) -> ( Vtx ` G ) = ( Vtx ` (/) ) )
4		vtxval0	|- ( Vtx ` (/) ) = (/)
5	3 4	eqtrdi	|- ( G = (/) -> ( Vtx ` G ) = (/) )
6	5	eleq2d	|- ( G = (/) -> ( U e. ( Vtx ` G ) <-> U e. (/) ) )
7	2 6	bitrid	|- ( G = (/) -> ( U e. V <-> U e. (/) ) )
8		noel	|- -. U e. (/)
9	8	pm2.21i	|- ( U e. (/) -> ( ( VtxDeg ` G ) ` U ) = 0 )
10	7 9	biimtrdi	|- ( G = (/) -> ( U e. V -> ( ( VtxDeg ` G ) ` U ) = 0 ) )
11	10	imp	|- ( ( G = (/) /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = 0 )