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 \in USGraph \land E \in Edg (G) \land Y \in E) \to \exists! y \in Vtx (G) E = \{Y, y\}$

Proof

Step	Hyp	Ref	Expression
1		usgruspgr	$⊢ G \in USGraph \to G \in USHGraph$
2		uspgredg2vtxeu	$⊢ (G \in USHGraph \land E \in Edg (G) \land Y \in E) \to \exists! y \in Vtx (G) E = \{Y, y\}$
3	1 2	syl3an1	$⊢ (G \in USGraph \land E \in Edg (G) \land Y \in E) \to \exists! y \in Vtx (G) E = \{Y, y\}$