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

Definition df-ray 25976
 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 25973 . 2 Ray
2 vp . . . . . . . 8
32cv 1648 . . . . . . 7
4 vn . . . . . . . . 9
54cv 1648 . . . . . . . 8
6 cee 25731 . . . . . . . 8
75, 6cfv 5413 . . . . . . 7
83, 7wcel 1721 . . . . . 6
9 va . . . . . . . 8
109cv 1648 . . . . . . 7
1110, 7wcel 1721 . . . . . 6
123, 10wne 2567 . . . . . 6
138, 11, 12w3a 936 . . . . 5
14 vr . . . . . . 7
1514cv 1648 . . . . . 6
16 vx . . . . . . . . . 10
1716cv 1648 . . . . . . . . 9
1810, 17cop 3777 . . . . . . . 8
19 coutsideof 25957 . . . . . . . 8 OutsideOf
203, 18, 19wbr 4172 . . . . . . 7 OutsideOf
2120, 16, 7crab 2670 . . . . . 6 OutsideOf
2215, 21wceq 1649 . . . . 5 OutsideOf
2313, 22wa 359 . . . 4 OutsideOf
24 cn 9956 . . . 4
2523, 4, 24wrex 2667 . . 3 OutsideOf
2625, 2, 9, 14coprab 6041 . 2 OutsideOf
271, 26wceq 1649 1 Ray OutsideOf
 Colors of variables: wff set class This definition is referenced by:  funray  25978  fvray  25979
 Copyright terms: Public domain W3C validator