Definition df-rp 12660

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	⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}

Detailed syntax breakdown of Definition df-rp

Step	Hyp	Ref	Expression
1		crp 12659	. 2 class ℝ+
2		cc0 10802	. . . 4 class 0
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1538	. . . 4 class 𝑥
5		clt 10940	. . . 4 class <
6	2, 4, 5	wbr 5070	. . 3 wff 0 < 𝑥
7		cr 10801	. . 3 class ℝ
8	6, 3, 7	crab 3067	. 2 class {𝑥 ∈ ℝ ∣ 0 < 𝑥}
9	1, 8	wceq 1539	1 wff ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}

This definition is referenced by:  elrp  12661  rpssre  12666  ioorp  13086