Theorem xrex 12999

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 11235	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11179	. . 3 ⊢ ℝ ∈ V
3		prex 5399	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7731	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2861	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2145  Vcvv 3457   ∪ cun 3905  {cpr 4587  ℝcr 11087  +∞cpnf 11228  -∞cmnf 11229  ℝ^*cxr 11230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394  ax-un 7722  ax-cnex 11144  ax-resscn 11145

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-un 3912  df-in 3914  df-ss 3924  df-sn 4586  df-pr 4588  df-uni 4868  df-xr 11235

This theorem is referenced by:  ixxval  13368  ixxf  13370  ixxex  13371  limsuple  15517  limsuplt  15518  limsupbnd1  15521  prdsds  17505  xrsle  17646  xrsbas  17648  letsr  18637  xrsadd  21497  xrsmul  21498  xrsds  21517  xrs1mnd  21547  xrs10  21548  xrs1cmn  21549  xrge0subm  21550  xrge0cmn  21551  znle  21643  leordtval2  23326  lecldbas  23333  ispsmet  24418  isxmet  24438  imasdsf1olem  24487  blfvalps  24497  nmoffn  24825  nmofval  24828  xrsxmet  24924  xrge0gsumle  24948  xrge0tsms  24949  xrlimcnp  27087  xrge00  33242  xrge0tsmsd  33301  xrhval  34320  ltex  42868  leex  42869  icof  45794  elicores  46108  fuzxrpmcn  46401  gsumge0cl  46944  ovnval2b  47125  volicorescl  47126  ovnsubaddlem1  47143