Metamath Proof Explorer

Theorem linethrueu

Description: There is a unique line going through any two distinct points. Theorem 6.19 of Schwabhauser p. 46. (Contributed by Scott Fenton, 29-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	linethrueu	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to \exists! x \in LinesEE (P \in x \land Q \in x)$

Proof

Step	Hyp	Ref	Expression
1		hilbert1.1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to \exists x \in LinesEE (P \in x \land Q \in x)$
2		simpr3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P \neq Q$
3		hilbert1.2	$⊢ P \neq Q \to \exists^{*} x \in LinesEE (P \in x \land Q \in x)$
4	2 3	syl	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to \exists^{*} x \in LinesEE (P \in x \land Q \in x)$
5		reu5	$⊢ \exists! x \in LinesEE (P \in x \land Q \in x) \leftrightarrow (\exists x \in LinesEE (P \in x \land Q \in x) \land \exists^{*} x \in LinesEE (P \in x \land Q \in x))$
6	1 4 5	sylanbrc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to \exists! x \in LinesEE (P \in x \land Q \in x)$