Theorem xrex 13002

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 5400	. . 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 5251  ax-pr 5395  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 4869  df-xr 11235

This theorem is referenced by:  ixxval  13371  ixxf  13373  ixxex  13374  limsuple  15519  limsuplt  15520  limsupbnd1  15523  prdsds  17507  xrsle  17648  xrsbas  17650  letsr  18639  xrsadd  21500  xrsmul  21501  xrsds  21520  xrs1mnd  21550  xrs10  21551  xrs1cmn  21552  xrge0subm  21553  xrge0cmn  21554  znle  21646  leordtval2  23330  lecldbas  23337  ispsmet  24422  isxmet  24442  imasdsf1olem  24491  blfvalps  24501  nmoffn  24829  nmofval  24832  xrsxmet  24928  xrge0gsumle  24952  xrge0tsms  24953  xrlimcnp  27091  xrge00  33247  xrge0tsmsd  33306  xrhval  34325  ltex  42873  leex  42874  icof  45793  elicores  46107  fuzxrpmcn  46400  gsumge0cl  46943  ovnval2b  47124  volicorescl  47125  ovnsubaddlem1  47142