Metamath Proof Explorer


Theorem uspgrf

Description: The edge function of a simple pseudograph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 13-Oct-2020)

Ref Expression
Hypotheses isuspgr.v V=VtxG
isuspgr.e E=iEdgG
Assertion uspgrf GUSHGraphE:domE1-1x𝒫V|x2

Proof

Step Hyp Ref Expression
1 isuspgr.v V=VtxG
2 isuspgr.e E=iEdgG
3 1 2 isuspgr GUSHGraphGUSHGraphE:domE1-1x𝒫V|x2
4 3 ibi GUSHGraphE:domE1-1x𝒫V|x2