Theorem xrex 12877

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

Syntax hints:   ∈ wcel 2110  Vcvv 3434   ∪ cun 3898  {cpr 4576  ℝcr 10997  +∞cpnf 11135  -∞cmnf 11136  ℝ^*cxr 11137

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 2112  ax-9 2120  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7663  ax-cnex 11054  ax-resscn 11055

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 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-sn 4575  df-pr 4577  df-uni 4858  df-xr 11142

This theorem is referenced by:  ixxval  13245  ixxf  13247  ixxex  13248  limsuple  15377  limsuplt  15378  limsupbnd1  15381  prdsds  17360  xrsle  17500  xrsbas  17502  letsr  18491  xrsadd  21315  xrsmul  21316  xrsds  21339  xrs1mnd  21370  xrs10  21371  xrs1cmn  21372  xrge0subm  21373  xrge0cmn  21374  znle  21466  leordtval2  23120  lecldbas  23127  ispsmet  24212  isxmet  24232  imasdsf1olem  24281  blfvalps  24291  nmoffn  24619  nmofval  24622  xrsxmet  24718  xrge0gsumle  24742  xrge0tsms  24743  xrlimcnp  26898  xrge00  32985  xrge0tsmsd  33032  xrhval  34021  ltex  42257  leex  42258  icof  45235  elicores  45552  fuzxrpmcn  45845  gsumge0cl  46388  ovnval2b  46569  volicorescl  46570  ovnsubaddlem1  46587