Metamath Proof Explorer


Theorem nbusgredgeu

Description: For each neighbor of a vertex there is exactly one edge between the vertex and its neighbor in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 27-Oct-2020)

Ref Expression
Hypothesis nbusgredgeu.e
|- E = ( Edg ` G )
Assertion nbusgredgeu
|- ( ( G e. USGraph /\ M e. ( G NeighbVtx N ) ) -> E! e e. E e = { M , N } )

Proof

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