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 | |
|
vtxdushgrfvedg.e | |
||
vtxdushgrfvedg.d | |
||
Assertion | vtxdumgr0nedg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtxdushgrfvedg.v | |
|
2 | vtxdushgrfvedg.e | |
|
3 | vtxdushgrfvedg.d | |
|
4 | umgruhgr | |
|
5 | 1 2 3 | vtxduhgr0nedg | |
6 | 4 5 | syl3an1 | |