This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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