Theorem xrex 12906

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438   ∪ cun 3903  {cpr 4581  ℝcr 11027  +∞cpnf 11165  -∞cmnf 11166  ℝ^*cxr 11167

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 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-sn 4580  df-pr 4582  df-uni 4862  df-xr 11172

This theorem is referenced by:  ixxval  13274  ixxf  13276  ixxex  13277  limsuple  15403  limsuplt  15404  limsupbnd1  15407  prdsds  17386  xrsle  17526  xrsbas  17528  letsr  18517  xrsadd  21310  xrsmul  21311  xrsds  21334  xrs1mnd  21365  xrs10  21366  xrs1cmn  21367  xrge0subm  21368  xrge0cmn  21369  znle  21461  leordtval2  23115  lecldbas  23122  ispsmet  24208  isxmet  24228  imasdsf1olem  24277  blfvalps  24287  nmoffn  24615  nmofval  24618  xrsxmet  24714  xrge0gsumle  24738  xrge0tsms  24739  xrlimcnp  26894  xrge00  32981  xrge0tsmsd  33028  xrhval  33984  ltex  42218  leex  42219  icof  45197  elicores  45515  fuzxrpmcn  45810  gsumge0cl  46353  ovnval2b  46534  volicorescl  46535  ovnsubaddlem1  46552