Definition df-bj-rrbar

Description: Definition of the set of extended real numbers. This aims to replace df-xr . (Contributed by BJ, 29-Jun-2019)

	Ref	Expression
Assertion	df-bj-rrbar	$$⊢\overline{ℝ}=ℝ\cup \left\{-\infty ,+\infty \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrbar	$$class\overline{ℝ}$$
1		cr	$$classℝ$$
2		cminfty	$$class-\infty$$
3		cpinfty	$$class+\infty$$
4	2 3	cpr	$$class\left\{-\infty ,+\infty \right\}$$
5	1 4	cun	$$class\left(ℝ\cup \left\{-\infty ,+\infty \right\}\right)$$
6	0 5	wceq	$$wff\overline{ℝ}=ℝ\cup \left\{-\infty ,+\infty \right\}$$