Theorem xrex

Description: The set of extended reals exists. (Contributed by NM, 24-Dec-2006)

	Ref	Expression
Assertion	xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-xr	$$⊢{ℝ}^{*}=ℝ\cup \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}$$
2		reex	$$⊢ℝ\in \mathrm{V}$$
3		prex	$$⊢\left\{\mathrm{+\infty },\mathrm{-\infty }\right\}\in \mathrm{V}$$
4	2 3	unex	$$⊢ℝ\cup \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}\in \mathrm{V}$$
5	1 4	eqeltri	$$⊢{ℝ}^{*}\in \mathrm{V}$$