Metamath Proof Explorer

Theorem uhgrfun

Description: The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017) (Revised by AV, 15-Dec-2020)

Ref Expression
Hypothesis uhgrfun.e E = iEdg G
Assertion uhgrfun G UHGraph Fun E


Step Hyp Ref Expression
1 uhgrfun.e E = iEdg G
2 eqid Vtx G = Vtx G
3 2 1 uhgrf G UHGraph E : dom E 𝒫 Vtx G
4 3 ffund G UHGraph Fun E