Metamath Proof Explorer

Theorem xrex

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

Ref Expression
Assertion xrex 
|- RR* e. _V

Proof

Step Hyp Ref Expression
1 df-xr 
 |-  RR* = ( RR u. { +oo , -oo } )
2 reex 
 |-  RR e. _V
3 prex 
 |-  { +oo , -oo } e. _V
4 2 3 unex 
 |-  ( RR u. { +oo , -oo } ) e. _V
5 1 4 eqeltri 
 |-  RR* e. _V