Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-outsideof | Structured version Visualization version GIF version |
Description: The outside of relationship. This relationship expresses that 𝑃, 𝐴, and 𝐵 fall on a line, but 𝑃 is not on the segment 𝐴𝐵. This definition is taken from theorem 6.4 of [Schwabhauser] p. 43, since it requires no dummy variables. (Contributed by Scott Fenton, 17-Oct-2013.) |
Ref | Expression |
---|---|
df-outsideof | ⊢ OutsideOf = ( Colinear ∖ Btwn ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coutsideof 34158 | . 2 class OutsideOf | |
2 | ccolin 34076 | . . 3 class Colinear | |
3 | cbtwn 26980 | . . 3 class Btwn | |
4 | 2, 3 | cdif 3863 | . 2 class ( Colinear ∖ Btwn ) |
5 | 1, 4 | wceq 1543 | 1 wff OutsideOf = ( Colinear ∖ Btwn ) |
Colors of variables: wff setvar class |
This definition is referenced by: broutsideof 34160 |
Copyright terms: Public domain | W3C validator |