Theorem xrex 11705

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 9957	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 9906	. . 3 ⊢ ℝ ∈ V
3		prex 4836	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 6854	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2684	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173   ∪ cun 3538  {cpr 4127  ℝcr 9814  +∞cpnf 9950  -∞cmnf 9951  ℝ^*cxr 9952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-sn 4126  df-pr 4128  df-uni 4373  df-xr 9957

This theorem is referenced by:  ixxval  12054  ixxf  12056  ixxex  12057  limsuple  14057  limsuplt  14058  limsupbnd1  14061  prdsds  15947  letsr  17050  xrsbas  19581  xrsadd  19582  xrsmul  19583  xrsle  19585  xrs1mnd  19603  xrs10  19604  xrs1cmn  19605  xrge0subm  19606  xrge0cmn  19607  xrsds  19608  znle  19703  leordtval2  20826  lecldbas  20833  ispsmet  21919  isxmet  21939  imasdsf1olem  21988  blfvalps  21998  nmoffn  22325  nmofval  22328  xrsxmet  22420  xrge0gsumle  22444  xrge0tsms  22445  xrlimcnp  24495  xrge00  29017  xrge0tsmsd  29116  xrhval  29390  icof  38406  elicores  38607  gsumge0cl  39264  ovnval2b  39442  volicorescl  39443  ovnsubaddlem1  39460