Theorem xrex

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

	Ref	Expression
Assertion	xrex	⊢ ℝ* ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-xr	⊢ ℝ* = ( ℝ ∪ { +∞ , -∞ } )
2		reex	⊢ ℝ ∈ V
3		prex	⊢ { +∞ , -∞ } ∈ V
4	2 3	unex	⊢ ( ℝ ∪ { +∞ , -∞ } ) ∈ V
5	1 4	eqeltri	⊢ ℝ* ∈ V