Metamath Proof Explorer

Theorem uhgredgiedgb

Description: In a hypergraph, a set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020)

Ref Expression
Hypothesis uhgredgiedgb.i ⊢I=iEdg⁡G
Assertion uhgredgiedgb ⊢G∈UHGraph→E∈Edg⁡G↔∃x∈dom⁡IE=I⁡x

Proof

Step Hyp Ref Expression
1 uhgredgiedgb.i ⊢I=iEdg⁡G
2 1 uhgrfun ⊢G∈UHGraph→Fun⁡I
3 1 edgiedgb ⊢Fun⁡I→E∈Edg⁡G↔∃x∈dom⁡IE=I⁡x
4 2 3 syl ⊢G∈UHGraph→E∈Edg⁡G↔∃x∈dom⁡IE=I⁡x