Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ray2 Unicode version

Definition df-ray2 26255
 Description: Definition of the ray xy degenerated or not. Definition 11 of [AitkenIBG] p. 4. (For my private use only. Don't use.) (Contributed by FL, 5-Mar-2016.)
Assertion
Ref Expression
df-ray2 ray Ibg PPoints PPoints PPoints btw
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-ray2
StepHypRef Expression
1 cray2 26254 . 2 ray
2 vf . . 3
3 cibg 26210 . . 3 Ibg
4 vx . . . 4
5 vy . . . 4
62cv 1631 . . . . 5
7 cpoints 26159 . . . . 5 PPoints
86, 7cfv 5271 . . . 4 PPoints
94cv 1631 . . . . . 6
105cv 1631 . . . . . 6
119, 10wne 2459 . . . . 5
12 cseg 26233 . . . . . . . 8
136, 12cfv 5271 . . . . . . 7
149, 10, 13co 5874 . . . . . 6
15 vz . . . . . . . . . 10
1615cv 1631 . . . . . . . . 9
17 cbtw 26209 . . . . . . . . . 10 btw
186, 17cfv 5271 . . . . . . . . 9 btw
199, 16, 18co 5874 . . . . . . . 8 btw
2010, 19wcel 1696 . . . . . . 7 btw
2120, 15, 8crab 2560 . . . . . 6 PPoints btw
2214, 21cun 3163 . . . . 5 PPoints btw
239csn 3653 . . . . 5
2411, 22, 23cif 3578 . . . 4 PPoints btw
254, 5, 8, 8, 24cmpt2 5876 . . 3 PPoints PPoints PPoints btw
262, 3, 25cmpt 4093 . 2 Ibg PPoints PPoints PPoints btw
271, 26wceq 1632 1 ray Ibg PPoints PPoints PPoints btw
 Colors of variables: wff set class This definition is referenced by:  isray2  26256  isray  26257
 Copyright terms: Public domain W3C validator