Description: The edge function in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | umgr2v2evtx.g | ||
Assertion | umgr2v2eiedg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | umgr2v2evtx.g | ||
2 | 1 | fveq2i | |
3 | simp1 | ||
4 | prex | ||
5 | opiedgfv | ||
6 | 3 4 5 | sylancl | |
7 | 2 6 | syl5eq |