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

Definition df-rp 10234
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 10233 . 2  class  RR+
2 cc0 8617 . . . 4  class  0
3 vx . . . . 5  set  x
43cv 1618 . . . 4  class  x
5 clt 8747 . . . 4  class  <
62, 4, 5wbr 3920 . . 3  wff  0  <  x
7 cr 8616 . . 3  class  RR
86, 3, 7crab 2512 . 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  10235  rpre  10239  ioorp  10605
  Copyright terms: Public domain W3C validator