Theorem edgopval

Description: The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020) (Revised by AV, 13-Oct-2020)

	Ref	Expression
Assertion	edgopval	|- ( ( V e. W /\ E e. X ) -> ( Edg ` <. V , E >. ) = ran E )

Proof

Step	Hyp	Ref	Expression
1		edgval	|- ( Edg ` <. V , E >. ) = ran ( iEdg ` <. V , E >. )
2		opiedgfv	|- ( ( V e. W /\ E e. X ) -> ( iEdg ` <. V , E >. ) = E )
3	2	rneqd	|- ( ( V e. W /\ E e. X ) -> ran ( iEdg ` <. V , E >. ) = ran E )
4	1 3	syl5eq	|- ( ( V e. W /\ E e. X ) -> ( Edg ` <. V , E >. ) = ran E )