Definition df-rp 11254

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

Step	Hyp	Ref	Expression
1		crp 11253	. 2 class RR+
2		cc0 9490	. . . 4 class 0
3		vx	. . . . 5 setvar x
4	3	cv 1436	. . . 4 class x
5		clt 9626	. . . 4 class <
6	2, 4, 5	wbr 4366	. . 3 wff 0 < x
7		cr 9489	. . 3 class RR
8	6, 3, 7	crab 2718	. 2 class { x e. RR | 0 < x }
9	1, 8	wceq 1437	1 wff RR+ = { x e. RR | 0 < x }

This definition is referenced by:  elrp  11255  rpre  11259  ioorp  11663