This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( ( V e. W /\ E e. X ) -> ( V Edg E ) = ran E )