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 \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		usgrupgr	$⊢ G \in USGraph \to G \in UPGraph$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3		eqid	$⊢ Edg (G) = Edg (G)$
4	2 3	upgredg2vtx	$⊢ (G \in UPGraph \land E \in Edg (G) \land Y \in E) \to \exists y \in Vtx (G) E = \{Y, y\}$
5	1 4	syl3an1	$⊢ (G \in USGraph \land E \in Edg (G) \land Y \in E) \to \exists y \in Vtx (G) E = \{Y, y\}$