Definition df-rp

Description: Define the set of positive reals. Definition of positive numbers in Apostol p. 20. (Contributed by NM, 27-Oct-2007)

	Ref	Expression
Assertion	df-rp	⊢ ℝ+ = { 𝑥 ∈ ℝ ∣ 0 < 𝑥 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crp	⊢ ℝ+
1		vx	⊢ 𝑥
2		cr	⊢ ℝ
3		cc0	⊢ 0
4		clt	⊢ <
5	1	cv	⊢ 𝑥
6	3 5 4	wbr	⊢ 0 < 𝑥
7	6 1 2	crab	⊢ { 𝑥 ∈ ℝ ∣ 0 < 𝑥 }
8	0 7	wceq	⊢ ℝ+ = { 𝑥 ∈ ℝ ∣ 0 < 𝑥 }