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 e. ( Edg ` G ) <-> E. x e. dom I E = ( 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 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 ) ) )