Theorem edgov

Description: The edges of a graph represented as ordered pair, shown as operation value. Although a little less intuitive, this representation is often used because it is shorter than the representation as function value of a graph given as ordered pair, see edgopval . The representation ran E for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020) (Revised by AV, 13-Oct-2020)

	Ref	Expression
Assertion	edgov	|- ( ( V e. W /\ E e. X ) -> ( V Edg E ) = ran E )

Proof

Step	Hyp	Ref	Expression
1		df-ov	|- ( V Edg E ) = ( Edg ` <. V , E >. )
2		edgopval	|- ( ( V e. W /\ E e. X ) -> ( Edg ` <. V , E >. ) = ran E )
3	1 2	syl5eq	|- ( ( V e. W /\ E e. X ) -> ( V Edg E ) = ran E )