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

Definition df-rp 10323
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 10322 . 2  class  RR+
2 cc0 8705 . . . 4  class  0
3 vx . . . . 5  set  x
43cv 1618 . . . 4  class  x
5 clt 8835 . . . 4  class  <
62, 4, 5wbr 3997 . . 3  wff  0  <  x
7 cr 8704 . . 3  class  RR
86, 3, 7crab 2522 . 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  10324  rpre  10328  ioorp  10694
  Copyright terms: Public domain W3C validator