ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-rp Unicode version

Definition df-rp 9598
Description: Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
Assertion
Ref Expression
df-rp  |-  RR+  =  { x  e.  RR  |  0  <  x }

Detailed syntax breakdown of Definition df-rp
StepHypRef Expression
1 crp 9597 . 2  class  RR+
2 cc0 7761 . . . 4  class  0
3 vx . . . . 5  setvar  x
43cv 1347 . . . 4  class  x
5 clt 7941 . . . 4  class  <
62, 4, 5wbr 3987 . . 3  wff  0  <  x
7 cr 7760 . . 3  class  RR
86, 3, 7crab 2452 . 2  class  { x  e.  RR  |  0  < 
x }
91, 8wceq 1348 1  wff  RR+  =  { x  e.  RR  |  0  <  x }
Colors of variables: wff set class
This definition is referenced by:  elrp  9599  rpre  9604  ioorp  9895
  Copyright terms: Public domain W3C validator