Metamath Proof Explorer


Theorem usgredgop

Description: An edge of a simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017) (Proof shortened by Alexander van der Vekens, 16-Dec-2017) (Revised by AV, 15-Oct-2020)

Ref Expression
Assertion usgredgop
|- ( ( G e. USGraph /\ E = ( iEdg ` G ) /\ X e. dom E ) -> ( ( E ` X ) = { M , N } <-> <. X , { M , N } >. e. E ) )

Proof

Step Hyp Ref Expression
1 usgrfun
 |-  ( G e. USGraph -> Fun ( iEdg ` G ) )
2 funeq
 |-  ( E = ( iEdg ` G ) -> ( Fun E <-> Fun ( iEdg ` G ) ) )
3 1 2 syl5ibrcom
 |-  ( G e. USGraph -> ( E = ( iEdg ` G ) -> Fun E ) )
4 3 imp
 |-  ( ( G e. USGraph /\ E = ( iEdg ` G ) ) -> Fun E )
5 funopfvb
 |-  ( ( Fun E /\ X e. dom E ) -> ( ( E ` X ) = { M , N } <-> <. X , { M , N } >. e. E ) )
6 4 5 stoic3
 |-  ( ( G e. USGraph /\ E = ( iEdg ` G ) /\ X e. dom E ) -> ( ( E ` X ) = { M , N } <-> <. X , { M , N } >. e. E ) )