Metamath Proof Explorer

Theorem edgiedgb

Description: A set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020) (Revised by AV, 8-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 edgiedgb.i ⊢I=iEdg⁡G
2 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
3 1 eqcomi ⊢iEdg⁡G=I
4 3 rneqi ⊢ran⁡iEdg⁡G=ran⁡I
5 2 4 eqtri ⊢Edg⁡G=ran⁡I
6 5 eleq2i ⊢E∈Edg⁡G↔E∈ran⁡I
7 elrnrexdmb ⊢Fun⁡I→E∈ran⁡I↔∃x∈dom⁡IE=I⁡x
8 6 7 bitrid ⊢Fun⁡I→E∈Edg⁡G↔∃x∈dom⁡IE=I⁡x