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 ) ) |
| 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 ) ) |