Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ray Unicode version

Definition df-ray 23935
 Description: Define the Ray function. This function generates the set of all points that lie on the ray starting at and passing through . Definition 6.8 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 21-Oct-2013.)
Assertion
Ref Expression
df-ray Ray OutsideOf
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-ray
StepHypRef Expression
1 cray 23932 . 2 Ray
2 vp . . . . . . . 8
32cv 1618 . . . . . . 7
4 vn . . . . . . . . 9
54cv 1618 . . . . . . . 8
6 cee 23690 . . . . . . . 8
75, 6cfv 4592 . . . . . . 7
83, 7wcel 1621 . . . . . 6
9 va . . . . . . . 8
109cv 1618 . . . . . . 7
1110, 7wcel 1621 . . . . . 6
123, 10wne 2412 . . . . . 6
138, 11, 12w3a 939 . . . . 5
14 vr . . . . . . 7
1514cv 1618 . . . . . 6
16 vx . . . . . . . . . 10
1716cv 1618 . . . . . . . . 9
1810, 17cop 3547 . . . . . . . 8
19 coutsideof 23916 . . . . . . . 8 OutsideOf
203, 18, 19wbr 3920 . . . . . . 7 OutsideOf
2120, 16, 7crab 2512 . . . . . 6 OutsideOf
2215, 21wceq 1619 . . . . 5 OutsideOf
2313, 22wa 360 . . . 4 OutsideOf
24 cn 9626 . . . 4
2523, 4, 24wrex 2510 . . 3 OutsideOf
2625, 2, 9, 14copab2 5711 . 2 OutsideOf
271, 26wceq 1619 1 Ray OutsideOf
 Colors of variables: wff set class This definition is referenced by:  funray  23937  fvray  23938
 Copyright terms: Public domain W3C validator