fvline2

Description: Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	fvline2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A Line B = \{x \in 𝔼 (N) \| x Colinear ⟨A, B⟩\}$

Step	Hyp	Ref	Expression
1		fvline	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A Line B = \{x \| x Colinear ⟨A, B⟩\}$
2		liness	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A Line B \subseteq 𝔼 (N)$
3	1 2	eqsstrrd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to \{x \| x Colinear ⟨A, B⟩\} \subseteq 𝔼 (N)$
4		df-ss	$⊢ \{x \| x Colinear ⟨A, B⟩\} \subseteq 𝔼 (N) \leftrightarrow \{x \| x Colinear ⟨A, B⟩\} \cap 𝔼 (N) = \{x \| x Colinear ⟨A, B⟩\}$
5	3 4	sylib	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to \{x \| x Colinear ⟨A, B⟩\} \cap 𝔼 (N) = \{x \| x Colinear ⟨A, B⟩\}$
6	1 5	eqtr4d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A Line B = \{x \| x Colinear ⟨A, B⟩\} \cap 𝔼 (N)$
7		dfrab2	$⊢ \{x \in 𝔼 (N) \| x Colinear ⟨A, B⟩\} = \{x \| x Colinear ⟨A, B⟩\} \cap 𝔼 (N)$
8	6 7	eqtr4di	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A Line B = \{x \in 𝔼 (N) \| x Colinear ⟨A, B⟩\}$

Metamath Proof Explorer