Metamath Proof Explorer


Theorem umgrf

Description: The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfn without explicitly specified domain of the edge function. (Contributed by AV, 24-Nov-2020)

Ref Expression
Hypotheses isumgr.v V=VtxG
isumgr.e E=iEdgG
Assertion umgrf GUMGraphE:domEx𝒫V|x=2

Proof

Step Hyp Ref Expression
1 isumgr.v V=VtxG
2 isumgr.e E=iEdgG
3 1 2 isumgrs GUMGraphGUMGraphE:domEx𝒫V|x=2
4 3 ibi GUMGraphE:domEx𝒫V|x=2