Theorem xrex 12887

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 11157	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11104	. . 3 ⊢ ℝ ∈ V
3		prex 5377	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7683	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2829	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3437   ∪ cun 3896  {cpr 4577  ℝcr 11012  +∞cpnf 11150  -∞cmnf 11151  ℝ^*cxr 11152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-resscn 11070

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-sn 4576  df-pr 4578  df-uni 4859  df-xr 11157

This theorem is referenced by:  ixxval  13255  ixxf  13257  ixxex  13258  limsuple  15387  limsuplt  15388  limsupbnd1  15391  prdsds  17370  xrsle  17510  xrsbas  17512  letsr  18501  xrsadd  21324  xrsmul  21325  xrsds  21348  xrs1mnd  21379  xrs10  21380  xrs1cmn  21381  xrge0subm  21382  xrge0cmn  21383  znle  21475  leordtval2  23128  lecldbas  23135  ispsmet  24220  isxmet  24240  imasdsf1olem  24289  blfvalps  24299  nmoffn  24627  nmofval  24630  xrsxmet  24726  xrge0gsumle  24750  xrge0tsms  24751  xrlimcnp  26906  xrge00  33002  xrge0tsmsd  33049  xrhval  34052  ltex  42363  leex  42364  icof  45340  elicores  45657  fuzxrpmcn  45950  gsumge0cl  46493  ovnval2b  46674  volicorescl  46675  ovnsubaddlem1  46692