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

Definition df-crcl 26199
 Description: Definition of a circle (degenerated or not). Definition 5 of [AitkenNG] p. 4. (For my private use only. Don't use.) (Contributed by FL, 5-Mar-2016.)
Assertion
Ref Expression
df-crcl Circle Ibcg PPoints PPoints PPoints segc
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-crcl
StepHypRef Expression
1 ccircle 26198 . 2 Circle
2 vg . . 3
3 cibcg 26181 . . 3 Ibcg
4 vx . . . 4
5 vy . . . 4
62cv 1622 . . . . 5
7 cpoints 26056 . . . . 5 PPoints
86, 7cfv 5255 . . . 4 PPoints
94cv 1622 . . . . . . 7
10 vu . . . . . . . 8
1110cv 1622 . . . . . . 7
12 cseg 26130 . . . . . . . 8
136, 12cfv 5255 . . . . . . 7
149, 11, 13co 5858 . . . . . 6
155cv 1622 . . . . . . 7
169, 15, 13co 5858 . . . . . 6
17 csegc 26180 . . . . . . 7 segc
186, 17cfv 5255 . . . . . 6 segc
1914, 16, 18wbr 4023 . . . . 5 segc
2019, 10, 8crab 2547 . . . 4 PPoints segc
214, 5, 8, 8, 20cmpt2 5860 . . 3 PPoints PPoints PPoints segc
222, 3, 21cmpt 4077 . 2 Ibcg PPoints PPoints PPoints segc
231, 22wceq 1623 1 Circle Ibcg PPoints PPoints PPoints segc
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator