Metamath Proof Explorer


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 V VtxDeg G U = 0

Proof

Step Hyp Ref Expression
1 vtxdgf.v V = Vtx G
2 1 eleq2i U V U Vtx G
3 fveq2 G = Vtx G = Vtx
4 vtxval0 Vtx =
5 3 4 eqtrdi G = Vtx G =
6 5 eleq2d G = U Vtx G U
7 2 6 syl5bb G = U V U
8 noel ¬ U
9 8 pm2.21i U VtxDeg G U = 0
10 7 9 syl6bi G = U V VtxDeg G U = 0
11 10 imp G = U V VtxDeg G U = 0