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

Definition df-btw 26211
Description: Definition of btw. (Contributed by FL, 1-Apr-2016.)
Assertion
Ref Expression
df-btw  |- btw  =  +g

Detailed syntax breakdown of Definition df-btw
StepHypRef Expression
1 cbtw 26209 . 2  class btw
2 cplusg 13224 . 2  class  +g
31, 2wceq 1632 1  wff btw  =  +g
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator