Metamath Proof Explorer

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