Metamath Proof Explorer

Theorem usgredg2vtx

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

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

Proof

Step Hyp Ref Expression
1 usgrupgr ⊢ G ∈ USGraph → G ∈ UPGraph
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 2 3 upgredg2vtx ⊢ G ∈ UPGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∃ y ∈ Vtx ⁡ G E = Y y
5 1 4 syl3an1 ⊢ G ∈ USGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∃ y ∈ Vtx ⁡ G E = Y y