Theorem xrex 11829

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 10078	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 10027	. . 3 ⊢ ℝ ∈ V
3		prex 4909	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 6956	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2697	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 1990  Vcvv 3200   ∪ cun 3572  {cpr 4179  ℝcr 9935  +∞cpnf 10071  -∞cmnf 10072  ℝ^*cxr 10073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437  df-xr 10078

This theorem is referenced by:  ixxval  12183  ixxf  12185  ixxex  12186  limsuple  14209  limsuplt  14210  limsupbnd1  14213  prdsds  16124  letsr  17227  xrsbas  19762  xrsadd  19763  xrsmul  19764  xrsle  19766  xrs1mnd  19784  xrs10  19785  xrs1cmn  19786  xrge0subm  19787  xrge0cmn  19788  xrsds  19789  znle  19884  leordtval2  21016  lecldbas  21023  ispsmet  22109  isxmet  22129  imasdsf1olem  22178  blfvalps  22188  nmoffn  22515  nmofval  22518  xrsxmet  22612  xrge0gsumle  22636  xrge0tsms  22637  xrlimcnp  24695  xrge00  29686  xrge0tsmsd  29785  xrhval  30062  icof  39411  elicores  39760  fuzxrpmcn  40054  gsumge0cl  40588  ovnval2b  40766  volicorescl  40767  ovnsubaddlem1  40784