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 ⁡ I E = 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 ⁡ I E = I ⁡ x
4 2 3 syl ⊢ G ∈ UHGraph → E ∈ Edg ⁡ G ↔ ∃ x ∈ dom ⁡ I E = I ⁡ x