Metamath Proof Explorer


Theorem vtxdumgr0nedg

Description: If a vertex in a multigraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017) (Revised by AV, 12-Dec-2020) (Proof shortened by AV, 15-Dec-2020)

Ref Expression
Hypotheses vtxdushgrfvedg.v V = Vtx G
vtxdushgrfvedg.e E = Edg G
vtxdushgrfvedg.d D = VtxDeg G
Assertion vtxdumgr0nedg G UMGraph U V D U = 0 ¬ v V U v 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 umgruhgr G UMGraph G UHGraph
5 1 2 3 vtxduhgr0nedg G UHGraph U V D U = 0 ¬ v V U v E
6 4 5 syl3an1 G UMGraph U V D U = 0 ¬ v V U v E