Theorem xrex 12900

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 11170	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11117	. . 3 ⊢ ℝ ∈ V
3		prex 5382	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7689	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2832	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3440   ∪ cun 3899  {cpr 4582  ℝcr 11025  +∞cpnf 11163  -∞cmnf 11164  ℝ^*cxr 11165

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083

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 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-sn 4581  df-pr 4583  df-uni 4864  df-xr 11170

This theorem is referenced by:  ixxval  13269  ixxf  13271  ixxex  13272  limsuple  15401  limsuplt  15402  limsupbnd1  15405  prdsds  17384  xrsle  17525  xrsbas  17527  letsr  18516  xrsadd  21340  xrsmul  21341  xrsds  21364  xrs1mnd  21395  xrs10  21396  xrs1cmn  21397  xrge0subm  21398  xrge0cmn  21399  znle  21491  leordtval2  23156  lecldbas  23163  ispsmet  24248  isxmet  24268  imasdsf1olem  24317  blfvalps  24327  nmoffn  24655  nmofval  24658  xrsxmet  24754  xrge0gsumle  24778  xrge0tsms  24779  xrlimcnp  26934  xrge00  33096  xrge0tsmsd  33155  xrhval  34175  ltex  42496  leex  42497  icof  45459  elicores  45775  fuzxrpmcn  46068  gsumge0cl  46611  ovnval2b  46792  volicorescl  46793  ovnsubaddlem1  46810