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	⊢ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑃 Colinear ⟨ 𝐴 , 𝐵 ⟩ ∧ ¬ 𝑃 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		df-outsideof	⊢ OutsideOf = ( Colinear ∖ Btwn )
2	1	breqi	⊢ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑃 ( Colinear ∖ Btwn ) ⟨ 𝐴 , 𝐵 ⟩ )
3		brdif	⊢ ( 𝑃 ( Colinear ∖ Btwn ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑃 Colinear ⟨ 𝐴 , 𝐵 ⟩ ∧ ¬ 𝑃 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
4	2 3	bitri	⊢ ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑃 Colinear ⟨ 𝐴 , 𝐵 ⟩ ∧ ¬ 𝑃 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )