Theorem xrex 12928

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430   ∪ cun 3888  {cpr 4570  ℝcr 11028  +∞cpnf 11167  -∞cmnf 11168  ℝ^*cxr 11169

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 5231  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086

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 3391  df-v 3432  df-un 3895  df-in 3897  df-ss 3907  df-sn 4569  df-pr 4571  df-uni 4852  df-xr 11174

This theorem is referenced by:  ixxval  13297  ixxf  13299  ixxex  13300  limsuple  15431  limsuplt  15432  limsupbnd1  15435  prdsds  17418  xrsle  17559  xrsbas  17561  letsr  18550  xrsadd  21375  xrsmul  21376  xrsds  21399  xrs1mnd  21430  xrs10  21431  xrs1cmn  21432  xrge0subm  21433  xrge0cmn  21434  znle  21526  leordtval2  23187  lecldbas  23194  ispsmet  24279  isxmet  24299  imasdsf1olem  24348  blfvalps  24358  nmoffn  24686  nmofval  24689  xrsxmet  24785  xrge0gsumle  24809  xrge0tsms  24810  xrlimcnp  26945  xrge00  33089  xrge0tsmsd  33149  xrhval  34178  ltex  42698  leex  42699  icof  45666  elicores  45981  fuzxrpmcn  46274  gsumge0cl  46817  ovnval2b  46998  volicorescl  46999  ovnsubaddlem1  47016