Theorem xrex 12946

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 11212	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11159	. . 3 ⊢ ℝ ∈ V
3		prex 5392	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7720	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2824	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3447   ∪ cun 3912  {cpr 4591  ℝcr 11067  +∞cpnf 11205  -∞cmnf 11206  ℝ^*cxr 11207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-sn 4590  df-pr 4592  df-uni 4872  df-xr 11212

This theorem is referenced by:  ixxval  13314  ixxf  13316  ixxex  13317  limsuple  15444  limsuplt  15445  limsupbnd1  15448  prdsds  17427  letsr  18552  xrsbas  21295  xrsadd  21296  xrsmul  21297  xrsle  21299  xrs1mnd  21321  xrs10  21322  xrs1cmn  21323  xrge0subm  21324  xrge0cmn  21325  xrsds  21326  znle  21446  leordtval2  23099  lecldbas  23106  ispsmet  24192  isxmet  24212  imasdsf1olem  24261  blfvalps  24271  nmoffn  24599  nmofval  24602  xrsxmet  24698  xrge0gsumle  24722  xrge0tsms  24723  xrlimcnp  26878  xrge00  32953  xrge0tsmsd  33002  xrhval  34008  ltex  42233  leex  42234  icof  45213  elicores  45531  fuzxrpmcn  45826  gsumge0cl  46369  ovnval2b  46550  volicorescl  46551  ovnsubaddlem1  46568