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