Theorem broutsideof

Description: Binary relation form of OutsideOf . Theorem 6.4 of Schwabhauser p. 43. (Contributed by Scott Fenton, 17-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	broutsideof	$$⊢P\mathrm{OutsideOf}⟨A,B⟩\leftrightarrow \left(P\mathrm{Colinear}⟨A,B⟩\wedge \neg P\mathrm{Btwn}⟨A,B⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-outsideof	$$⊢\mathrm{OutsideOf}=\mathrm{Colinear}\setminus \mathrm{Btwn}$$
2	1	breqi	$$⊢P\mathrm{OutsideOf}⟨A,B⟩\leftrightarrow P\left(\mathrm{Colinear}\setminus \mathrm{Btwn}\right)⟨A,B⟩$$
3		brdif	$$⊢P\left(\mathrm{Colinear}\setminus \mathrm{Btwn}\right)⟨A,B⟩\leftrightarrow \left(P\mathrm{Colinear}⟨A,B⟩\wedge \neg P\mathrm{Btwn}⟨A,B⟩\right)$$
4	2 3	bitri	$$⊢P\mathrm{OutsideOf}⟨A,B⟩\leftrightarrow \left(P\mathrm{Colinear}⟨A,B⟩\wedge \neg P\mathrm{Btwn}⟨A,B⟩\right)$$