MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rp Unicode version

Definition df-rp 10506
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 10505 . 2  class  RR+
2 cc0 8884 . . . 4  class  0
3 vx . . . . 5  set  x
43cv 1646 . . . 4  class  x
5 clt 9014 . . . 4  class  <
62, 4, 5wbr 4125 . . 3  wff  0  <  x
7 cr 8883 . . 3  class  RR
86, 3, 7crab 2632 . 2  class  { x  e.  RR  |  0  < 
x }
91, 8wceq 1647 1  wff  RR+  =  { x  e.  RR  |  0  <  x }
Colors of variables: wff set class
This definition is referenced by:  elrp  10507  rpre  10511  ioorp  10880
  Copyright terms: Public domain W3C validator