Step |
Hyp |
Ref |
Expression |
1 |
|
nbusgredgeu.e |
|- E = ( Edg ` G ) |
2 |
1
|
nbusgreledg |
|- ( G e. USGraph -> ( M e. ( G NeighbVtx N ) <-> { M , N } e. E ) ) |
3 |
2
|
biimpa |
|- ( ( G e. USGraph /\ M e. ( G NeighbVtx N ) ) -> { M , N } e. E ) |
4 |
|
eqeq1 |
|- ( e = { M , N } -> ( e = { M , N } <-> { M , N } = { M , N } ) ) |
5 |
4
|
adantl |
|- ( ( ( G e. USGraph /\ M e. ( G NeighbVtx N ) ) /\ e = { M , N } ) -> ( e = { M , N } <-> { M , N } = { M , N } ) ) |
6 |
|
eqidd |
|- ( ( G e. USGraph /\ M e. ( G NeighbVtx N ) ) -> { M , N } = { M , N } ) |
7 |
3 5 6
|
rspcedvd |
|- ( ( G e. USGraph /\ M e. ( G NeighbVtx N ) ) -> E. e e. E e = { M , N } ) |
8 |
|
rmoeq |
|- E* e e. E e = { M , N } |
9 |
|
reu5 |
|- ( E! e e. E e = { M , N } <-> ( E. e e. E e = { M , N } /\ E* e e. E e = { M , N } ) ) |
10 |
7 8 9
|
sylanblrc |
|- ( ( G e. USGraph /\ M e. ( G NeighbVtx N ) ) -> E! e e. E e = { M , N } ) |