Theorem xrex 11867

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 10116	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 10065	. . 3 ⊢ ℝ ∈ V
3		prex 4939	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 6998	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2726	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2030  Vcvv 3231   ∪ cun 3605  {cpr 4212  ℝcr 9973  +∞cpnf 10109  -∞cmnf 10110  ℝ^*cxr 10111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-sn 4211  df-pr 4213  df-uni 4469  df-xr 10116

This theorem is referenced by:  ixxval  12221  ixxf  12223  ixxex  12224  limsuple  14253  limsuplt  14254  limsupbnd1  14257  prdsds  16171  letsr  17274  xrsbas  19810  xrsadd  19811  xrsmul  19812  xrsle  19814  xrs1mnd  19832  xrs10  19833  xrs1cmn  19834  xrge0subm  19835  xrge0cmn  19836  xrsds  19837  znle  19932  leordtval2  21064  lecldbas  21071  ispsmet  22156  isxmet  22176  imasdsf1olem  22225  blfvalps  22235  nmoffn  22562  nmofval  22565  xrsxmet  22659  xrge0gsumle  22683  xrge0tsms  22684  xrlimcnp  24740  xrge00  29814  xrge0tsmsd  29913  xrhval  30190  icof  39725  elicores  40078  fuzxrpmcn  40372  gsumge0cl  40906  ovnval2b  41087  volicorescl  41088  ovnsubaddlem1  41105