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

Definition df-rp 10287
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 10286 . 2  class  RR+
2 cc0 8670 . . . 4  class  0
3 vx . . . . 5  set  x
43cv 1618 . . . 4  class  x
5 clt 8800 . . . 4  class  <
62, 4, 5wbr 3963 . . 3  wff  0  <  x
7 cr 8669 . . 3  class  RR
86, 3, 7crab 2519 . 2  class  { x  e.  RR  |  0  < 
x }
91, 8wceq 1619 1  wff  RR+  =  { x  e.  RR  |  0  <  x }
Colors of variables: wff set class
This definition is referenced by:  elrp  10288  rpre  10292  ioorp  10658
  Copyright terms: Public domain W3C validator