Metamath Proof Explorer


Theorem umgredgss

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 GUMGraphEdgGx𝒫VtxG|x=2

Proof

Step Hyp Ref Expression
1 edgval EdgG=raniEdgG
2 eqid VtxG=VtxG
3 eqid iEdgG=iEdgG
4 2 3 umgrf GUMGraphiEdgG:domiEdgGx𝒫VtxG|x=2
5 4 frnd GUMGraphraniEdgGx𝒫VtxG|x=2
6 1 5 eqsstrid GUMGraphEdgGx𝒫VtxG|x=2