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	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	nbusgredgeu	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) → ∃! 𝑒 ∈ 𝐸 𝑒 = { 𝑀 , 𝑁 } )

Proof

Step	Hyp	Ref	Expression
1		nbusgredgeu.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
2	1	nbusgreledg	⊢ ( 𝐺 ∈ USGraph → ( 𝑀 ∈ ( 𝐺 NeighbVtx 𝑁 ) ↔ { 𝑀 , 𝑁 } ∈ 𝐸 ) )
3	2	biimpa	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) → { 𝑀 , 𝑁 } ∈ 𝐸 )
4		eqeq1	⊢ ( 𝑒 = { 𝑀 , 𝑁 } → ( 𝑒 = { 𝑀 , 𝑁 } ↔ { 𝑀 , 𝑁 } = { 𝑀 , 𝑁 } ) )
5	4	adantl	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) ∧ 𝑒 = { 𝑀 , 𝑁 } ) → ( 𝑒 = { 𝑀 , 𝑁 } ↔ { 𝑀 , 𝑁 } = { 𝑀 , 𝑁 } ) )
6		eqidd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) → { 𝑀 , 𝑁 } = { 𝑀 , 𝑁 } )
7	3 5 6	rspcedvd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) → ∃ 𝑒 ∈ 𝐸 𝑒 = { 𝑀 , 𝑁 } )
8		rmoeq	⊢ ∃* 𝑒 ∈ 𝐸 𝑒 = { 𝑀 , 𝑁 }
9		reu5	⊢ ( ∃! 𝑒 ∈ 𝐸 𝑒 = { 𝑀 , 𝑁 } ↔ ( ∃ 𝑒 ∈ 𝐸 𝑒 = { 𝑀 , 𝑁 } ∧ ∃* 𝑒 ∈ 𝐸 𝑒 = { 𝑀 , 𝑁 } ) )
10	7 8 9	sylanblrc	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) → ∃! 𝑒 ∈ 𝐸 𝑒 = { 𝑀 , 𝑁 } )