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 ⊢ 𝐸 = ( 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 𝑁 ) ) → ∃! 𝑒 ∈ 𝐸 𝑒 = { 𝑀 , 𝑁 } )