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

Definition df-seg2 25297
 Description: Definition of the segment xy degenerated or not. Definition 8 of [AitkenIBG] p. 4. (For my private use only. Don't use.) (Contributed by FL, 28-Feb-2016.)
Assertion
Ref Expression
df-seg2 Ibg PPoints PPoints PPoints btw
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-seg2
StepHypRef Expression
1 cseg 25296 . 2
2 vf . . 3
3 cibg 25273 . . 3 Ibg
4 vx . . . 4
5 vy . . . 4
62cv 1618 . . . . 5
7 cpoints 25222 . . . . 5 PPoints
86, 7cfv 4592 . . . 4 PPoints
94cv 1618 . . . . . 6
105cv 1618 . . . . . 6
119, 10wne 2412 . . . . 5
12 vz . . . . . . . . 9
1312cv 1618 . . . . . . . 8
14 cbtw 25272 . . . . . . . . . 10 btw
156, 14cfv 4592 . . . . . . . . 9 btw
169, 10, 15co 5710 . . . . . . . 8 btw
1713, 16wcel 1621 . . . . . . 7 btw
1812, 4weq 1620 . . . . . . 7
1912, 5weq 1620 . . . . . . 7
2017, 18, 19w3o 938 . . . . . 6 btw
2120, 12, 8crab 2512 . . . . 5 PPoints btw
229csn 3544 . . . . 5
2311, 21, 22cif 3470 . . . 4 PPoints btw
244, 5, 8, 8, 23cmpt2 5712 . . 3 PPoints PPoints PPoints btw
252, 3, 24cmpt 3974 . 2 Ibg PPoints PPoints PPoints btw
261, 25wceq 1619 1 Ibg PPoints PPoints PPoints btw
 Colors of variables: wff set class This definition is referenced by:  sgplpte21  25298  sgplpte22  25304
 Copyright terms: Public domain W3C validator