Theorem xrex 12953

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 11219	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11166	. . 3 ⊢ ℝ ∈ V
3		prex 5395	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7723	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2825	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3450   ∪ cun 3915  {cpr 4594  ℝcr 11074  +∞cpnf 11212  -∞cmnf 11213  ℝ^*cxr 11214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-sn 4593  df-pr 4595  df-uni 4875  df-xr 11219

This theorem is referenced by:  ixxval  13321  ixxf  13323  ixxex  13324  limsuple  15451  limsuplt  15452  limsupbnd1  15455  prdsds  17434  letsr  18559  xrsbas  21302  xrsadd  21303  xrsmul  21304  xrsle  21306  xrs1mnd  21328  xrs10  21329  xrs1cmn  21330  xrge0subm  21331  xrge0cmn  21332  xrsds  21333  znle  21453  leordtval2  23106  lecldbas  23113  ispsmet  24199  isxmet  24219  imasdsf1olem  24268  blfvalps  24278  nmoffn  24606  nmofval  24609  xrsxmet  24705  xrge0gsumle  24729  xrge0tsms  24730  xrlimcnp  26885  xrge00  32960  xrge0tsmsd  33009  xrhval  34015  ltex  42240  leex  42241  icof  45220  elicores  45538  fuzxrpmcn  45833  gsumge0cl  46376  ovnval2b  46557  volicorescl  46558  ovnsubaddlem1  46575