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	$$⊢ℝ=𝑹\times \left\{0_{𝑹}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cr	$$classℝ$$
1		cnr	$$class𝑹$$
2		c0r	$$class{0}_{𝑹}$$
3	2	csn	$$class\left\{0_{𝑹}\right\}$$
4	1 3	cxp	$$class\left(𝑹\times \left\{0_{𝑹}\right\}\right)$$
5	0 4	wceq	$$wffℝ=𝑹\times \left\{0_{𝑹}\right\}$$