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	$$⊢{ℝ}^{+}=\left\{x\in ℝ|0<x\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crp	$$class{ℝ}^{+}$$
1		vx	$$setvarx$$
2		cr	$$classℝ$$
3		cc0	$$class0$$
4		clt	$$class<$$
5	1	cv	$$setvarx$$
6	3 5 4	wbr	$$wff0<x$$
7	6 1 2	crab	$$class\left\{x\in ℝ|0<x\right\}$$
8	0 7	wceq	$$wff{ℝ}^{+}=\left\{x\in ℝ|0<x\right\}$$