Definition df-r

Description: Define the set of real numbers. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	df-r	⊢ ℝ = ( R × { 0R } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cr	⊢ ℝ
1		cnr	⊢ R
2		c0r	⊢ 0R
3	2	csn	⊢ { 0R }
4	1 3	cxp	⊢ ( R × { 0R } )
5	0 4	wceq	⊢ ℝ = ( R × { 0R } )