Metamath Proof Explorer

Theorem usgredgreu

Description: For a vertex incident to an edge there is exactly one other vertex incident to the edge. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020)

		Ref	Expression
	Hypotheses	usgredg3.v	$⊢ V = Vtx (G)$
		usgredg3.e	$⊢ E = iEdg (G)$
	Assertion	usgredgreu	$⊢ (G \in USGraph \land X \in dom E \land Y \in E (X)) \to \exists! y \in V E (X) = \{Y, y\}$

Proof

Step	Hyp	Ref	Expression
1		usgredg3.v	$⊢ V = Vtx (G)$
2		usgredg3.e	$⊢ E = iEdg (G)$
3	1 2	usgredg4	$⊢ (G \in USGraph \land X \in dom E \land Y \in E (X)) \to \exists y \in V E (X) = \{Y, y\}$
4		eqtr2	$⊢ (E (X) = \{Y, y\} \land E (X) = \{Y, x\}) \to \{Y, y\} = \{Y, x\}$
5		vex	$⊢ y \in V$
6		vex	$⊢ x \in V$
7	5 6	preqr2	$⊢ \{Y, y\} = \{Y, x\} \to y = x$
8	4 7	syl	$⊢ (E (X) = \{Y, y\} \land E (X) = \{Y, x\}) \to y = x$
9	8	a1i	$⊢ ((G \in USGraph \land X \in dom E \land Y \in E (X)) \land (y \in V \land x \in V)) \to ((E (X) = \{Y, y\} \land E (X) = \{Y, x\}) \to y = x)$
10	9	ralrimivva	$⊢ (G \in USGraph \land X \in dom E \land Y \in E (X)) \to \forall y \in V \forall x \in V ((E (X) = \{Y, y\} \land E (X) = \{Y, x\}) \to y = x)$
11		preq2	$⊢ y = x \to \{Y, y\} = \{Y, x\}$
12	11	eqeq2d	$⊢ y = x \to (E (X) = \{Y, y\} \leftrightarrow E (X) = \{Y, x\})$
13	12	reu4	$⊢ \exists! y \in V E (X) = \{Y, y\} \leftrightarrow (\exists y \in V E (X) = \{Y, y\} \land \forall y \in V \forall x \in V ((E (X) = \{Y, y\} \land E (X) = \{Y, x\}) \to y = x))$
14	3 10 13	sylanbrc	$⊢ (G \in USGraph \land X \in dom E \land Y \in E (X)) \to \exists! y \in V E (X) = \{Y, y\}$