Metamath Proof Explorer


Theorem usgrfun

Description: The edge function of a simple graph is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017) (Revised by AV, 13-Oct-2020)

Ref Expression
Assertion usgrfun G USGraph Fun iEdg G

Proof

Step Hyp Ref Expression
1 eqid Vtx G = Vtx G
2 eqid iEdg G = iEdg G
3 1 2 usgrfs G USGraph iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x = 2
4 f1fun iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x = 2 Fun iEdg G
5 3 4 syl G USGraph Fun iEdg G