Metamath Proof Explorer


Theorem usgrnloopv

Description: In a simple graph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 26-Jan-2018) (Revised by AV, 17-Oct-2020) (Proof shortened by AV, 11-Dec-2020)

Ref Expression
Hypothesis usgrnloopv.e E = iEdg G
Assertion usgrnloopv G USGraph M W E X = M N M N

Proof

Step Hyp Ref Expression
1 usgrnloopv.e E = iEdg G
2 usgrumgr G USGraph G UMGraph
3 1 umgrnloopv G UMGraph M W E X = M N M N
4 2 3 sylan G USGraph M W E X = M N M N