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	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		usgruspgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
2		uspgredg2vtxeu	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } )
3	1 2	syl3an1	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } )