Theorem xrex 11773

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 10023	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 9972	. . 3 ⊢ ℝ ∈ V
3		prex 4875	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 6910	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2700	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 1992  Vcvv 3191   ∪ cun 3558  {cpr 4155  ℝcr 9880  +∞cpnf 10016  -∞cmnf 10017  ℝ^*cxr 10018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rex 2918  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-sn 4154  df-pr 4156  df-uni 4408  df-xr 10023

This theorem is referenced by:  ixxval  12122  ixxf  12124  ixxex  12125  limsuple  14138  limsuplt  14139  limsupbnd1  14142  prdsds  16040  letsr  17143  xrsbas  19676  xrsadd  19677  xrsmul  19678  xrsle  19680  xrs1mnd  19698  xrs10  19699  xrs1cmn  19700  xrge0subm  19701  xrge0cmn  19702  xrsds  19703  znle  19798  leordtval2  20921  lecldbas  20928  ispsmet  22014  isxmet  22034  imasdsf1olem  22083  blfvalps  22093  nmoffn  22420  nmofval  22423  xrsxmet  22515  xrge0gsumle  22539  xrge0tsms  22540  xrlimcnp  24590  xrge00  29463  xrge0tsmsd  29562  xrhval  29836  icof  38871  elicores  39158  gsumge0cl  39882  ovnval2b  40060  volicorescl  40061  ovnsubaddlem1  40078