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

Definition df-angle 25324
 Description: Definition of an angle. Definition 17 of [AitkenIBG] p. 10. The angles can't be degenerated. Contrary to the concept of degenerated line or segment, the concept of degenerated angle no longer simplifies the wording. (For my private use only. Don't use.) (Contributed by FL, 7-Apr-2016.)
Assertion
Ref Expression
df-angle angle Ibg PPointsdWords ray ray
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-angle
StepHypRef Expression
1 cangle 25323 . 2 angle
2 vg . . 3
3 cibg 25273 . . 3 Ibg
4 vw . . . 4
52cv 1618 . . . . . 6
6 cpoints 25222 . . . . . 6 PPoints
75, 6cfv 4592 . . . . 5 PPoints
8 c3 9676 . . . . 5
9 cdwords 25150 . . . . 5 dWords
107, 8, 9co 5710 . . . 4 PPointsdWords
11 c2 9675 . . . . . . 7
124cv 1618 . . . . . . 7
1311, 12cfv 4592 . . . . . 6
14 c1 8618 . . . . . . 7
1514, 12cfv 4592 . . . . . 6
16 cray2 25317 . . . . . . 7 ray
175, 16cfv 4592 . . . . . 6 ray
1813, 15, 17co 5710 . . . . 5 ray
198, 12cfv 4592 . . . . . 6
2013, 19, 17co 5710 . . . . 5 ray
2118, 20cun 3076 . . . 4 ray ray
224, 10, 21cmpt 3974 . . 3 PPointsdWords ray ray
232, 3, 22cmpt 3974 . 2 Ibg PPointsdWords ray ray
241, 23wceq 1619 1 angle Ibg PPointsdWords ray ray
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator