Theorem xrex 12935

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

Assertion

Ref	Expression
xrex	⊢ ℝ* ∈ V

Proof of Theorem xrex

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432   ∪ cun 3888  {cpr 4564  ℝcr 11035  +∞cpnf 11174  -∞cmnf 11175  ℝ^*cxr 11176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-un 3895  df-in 3897  df-ss 3907  df-sn 4563  df-pr 4565  df-uni 4846  df-xr 11181

This theorem is referenced by:  ixxval  13304  ixxf  13306  ixxex  13307  limsuple  15438  limsuplt  15439  limsupbnd1  15442  prdsds  17425  xrsle  17566  xrsbas  17568  letsr  18557  xrsadd  21372  xrsmul  21373  xrsds  21392  xrs1mnd  21422  xrs10  21423  xrs1cmn  21424  xrge0subm  21425  xrge0cmn  21426  znle  21518  leordtval2  23202  lecldbas  23209  ispsmet  24294  isxmet  24314  imasdsf1olem  24363  blfvalps  24373  nmoffn  24701  nmofval  24704  xrsxmet  24800  xrge0gsumle  24824  xrge0tsms  24825  xrlimcnp  26957  xrge00  33100  xrge0tsmsd  33161  xrhval  34209  ltex  42736  leex  42737  icof  45671  elicores  45985  fuzxrpmcn  46278  gsumge0cl  46821  ovnval2b  47002  volicorescl  47003  ovnsubaddlem1  47020