Description: A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 20-Jan-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 0pthon.v | ||
Assertion | 0pthon1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0pthon.v | ||
2 | eqidd | ||
3 | 1fv | ||
4 | 2 3 | mpdan | |
5 | 1 | 0pthon | |
6 | 4 5 | syl |