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 e. ( Edg ` G ) <-> E. x e. dom I E = ( I ` x ) ) ) |
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 e. ( Edg ` G ) <-> E e. ran I ) |
7 | elrnrexdmb | |- ( Fun I -> ( E e. ran I <-> E. x e. dom I E = ( I ` x ) ) ) |
|
8 | 6 7 | syl5bb | |- ( Fun I -> ( E e. ( Edg ` G ) <-> E. x e. dom I E = ( I ` x ) ) ) |