Theorem xrex 13012

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 11248	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11192	. . 3 ⊢ ℝ ∈ V
3		prex 5411	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7744	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2859	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455   ∪ cun 3904  {cpr 4592  ℝcr 11100  +∞cpnf 11241  -∞cmnf 11242  ℝ^*cxr 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3911  df-in 3913  df-ss 3923  df-sn 4591  df-pr 4593  df-uni 4874  df-xr 11248

This theorem is referenced by:  ixxval  13381  ixxf  13383  ixxex  13384  limsuple  15531  limsuplt  15532  limsupbnd1  15535  prdsds  17518  xrsle  17659  xrsbas  17661  letsr  18650  xrsadd  21521  xrsmul  21522  xrsds  21541  xrs1mnd  21571  xrs10  21572  xrs1cmn  21573  xrge0subm  21574  xrge0cmn  21575  znle  21667  leordtval2  23350  lecldbas  23357  ispsmet  24442  isxmet  24462  imasdsf1olem  24511  blfvalps  24521  nmoffn  24849  nmofval  24852  xrsxmet  24948  xrge0gsumle  24972  xrge0tsms  24973  xrlimcnp  27111  xrge00  33312  xrge0tsmsd  33371  xrhval  34386  ltex  42991  leex  42992  icof  45915  elicores  46229  fuzxrpmcn  46522  gsumge0cl  47065  ovnval2b  47246  volicorescl  47247  ovnsubaddlem1  47264