Description: The set of edges of a multigraph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 25-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | umgredgss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | edgval | |
|
2 | eqid | |
|
3 | eqid | |
|
4 | 2 3 | umgrf | |
5 | 4 | frnd | |
6 | 1 5 | eqsstrid | |