Metamath Proof Explorer

Theorem usgredg2vtxeu

Description: For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020) (Proof shortened by AV, 6-Dec-2020)

Ref Expression
Assertion usgredg2vtxeu ⊢ G ∈ USGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y

Proof

Step Hyp Ref Expression
1 usgruspgr ⊢ G ∈ USGraph → G ∈ USHGraph
2 uspgredg2vtxeu ⊢ G ∈ USHGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y
3 1 2 syl3an1 ⊢ G ∈ USGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y