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 ∈ USGraph ∧ M ∈ G NeighbVtx N → ∃! e ∈ E e = M N

Proof

Step Hyp Ref Expression
1 nbusgredgeu.e ⊢ E = Edg ⁡ G
2 1 nbusgreledg ⊢ G ∈ USGraph → M ∈ G NeighbVtx N ↔ M N ∈ E
3 2 biimpa ⊢ G ∈ USGraph ∧ M ∈ G NeighbVtx N → M N ∈ E
4 eqeq1 ⊢ e = M N → e = M N ↔ M N = M N
5 4 adantl ⊢ G ∈ USGraph ∧ M ∈ G NeighbVtx N ∧ e = M N → e = M N ↔ M N = M N
6 eqidd ⊢ G ∈ USGraph ∧ M ∈ G NeighbVtx N → M N = M N
7 3 5 6 rspcedvd ⊢ G ∈ USGraph ∧ M ∈ G NeighbVtx N → ∃ e ∈ E e = M N
8 rmoeq ⊢ ∃* e ∈ E e = M N
9 reu5 ⊢ ∃! e ∈ E e = M N ↔ ∃ e ∈ E e = M N ∧ ∃* e ∈ E e = M N
10 7 8 9 sylanblrc ⊢ G ∈ USGraph ∧ M ∈ G NeighbVtx N → ∃! e ∈ E e = M N