Theorem xrex 12912

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 11182	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11129	. . 3 ⊢ ℝ ∈ V
3		prex 5384	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7699	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2833	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442   ∪ cun 3901  {cpr 4584  ℝcr 11037  +∞cpnf 11175  -∞cmnf 11176  ℝ^*cxr 11177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-un 3908  df-in 3910  df-ss 3920  df-sn 4583  df-pr 4585  df-uni 4866  df-xr 11182

This theorem is referenced by:  ixxval  13281  ixxf  13283  ixxex  13284  limsuple  15413  limsuplt  15414  limsupbnd1  15417  prdsds  17396  xrsle  17537  xrsbas  17539  letsr  18528  xrsadd  21352  xrsmul  21353  xrsds  21376  xrs1mnd  21407  xrs10  21408  xrs1cmn  21409  xrge0subm  21410  xrge0cmn  21411  znle  21503  leordtval2  23168  lecldbas  23175  ispsmet  24260  isxmet  24280  imasdsf1olem  24329  blfvalps  24339  nmoffn  24667  nmofval  24670  xrsxmet  24766  xrge0gsumle  24790  xrge0tsms  24791  xrlimcnp  26946  xrge00  33106  xrge0tsmsd  33166  xrhval  34195  ltex  42609  leex  42610  icof  45571  elicores  45887  fuzxrpmcn  46180  gsumge0cl  46723  ovnval2b  46904  volicorescl  46905  ovnsubaddlem1  46922