Theorem broutsideof 36122

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.)

Assertion

Ref	Expression
broutsideof	⊢ (𝑃OutsideOf⟨𝐴, 𝐵⟩ ↔ (𝑃 Colinear ⟨𝐴, 𝐵⟩ ∧ ¬ 𝑃 Btwn ⟨𝐴, 𝐵⟩))

Proof of Theorem broutsideof

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∖ cdif 3948  ⟨cop 4632   class class class wbr 5143   Btwn cbtwn 28904   Colinear ccolin 36038  OutsideOfcoutsideof 36120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-br 5144  df-outsideof 36121

This theorem is referenced by:  broutsideof2  36123  outsideofrflx  36128  outsidele  36133  outsideofcol  36134