# 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}=\mathrm{iEdg}\left({G}\right)$
Assertion edgiedgb ${⊢}\mathrm{Fun}{I}\to \left({E}\in \mathrm{Edg}\left({G}\right)↔\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{E}={I}\left({x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 edgiedgb.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
2 edgval ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{ran}\mathrm{iEdg}\left({G}\right)$
3 1 eqcomi ${⊢}\mathrm{iEdg}\left({G}\right)={I}$
4 3 rneqi ${⊢}\mathrm{ran}\mathrm{iEdg}\left({G}\right)=\mathrm{ran}{I}$
5 2 4 eqtri ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{ran}{I}$
6 5 eleq2i ${⊢}{E}\in \mathrm{Edg}\left({G}\right)↔{E}\in \mathrm{ran}{I}$
7 elrnrexdmb ${⊢}\mathrm{Fun}{I}\to \left({E}\in \mathrm{ran}{I}↔\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{E}={I}\left({x}\right)\right)$
8 6 7 syl5bb ${⊢}\mathrm{Fun}{I}\to \left({E}\in \mathrm{Edg}\left({G}\right)↔\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{E}={I}\left({x}\right)\right)$