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 ) ) )