Theorem xrex 12656

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 10944	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 10893	. . 3 ⊢ ℝ ∈ V
3		prex 5350	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7574	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2835	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3422   ∪ cun 3881  {cpr 4560  ℝcr 10801  +∞cpnf 10937  -∞cmnf 10938  ℝ^*cxr 10939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559  df-pr 4561  df-uni 4837  df-xr 10944

This theorem is referenced by:  ixxval  13016  ixxf  13018  ixxex  13019  limsuple  15115  limsuplt  15116  limsupbnd1  15119  prdsds  17092  letsr  18226  xrsbas  20526  xrsadd  20527  xrsmul  20528  xrsle  20530  xrs1mnd  20548  xrs10  20549  xrs1cmn  20550  xrge0subm  20551  xrge0cmn  20552  xrsds  20553  znle  20652  leordtval2  22271  lecldbas  22278  ispsmet  23365  isxmet  23385  imasdsf1olem  23434  blfvalps  23444  nmoffn  23781  nmofval  23784  xrsxmet  23878  xrge0gsumle  23902  xrge0tsms  23903  xrlimcnp  26023  xrge00  31197  xrge0tsmsd  31219  xrhval  31868  icof  42648  elicores  42961  fuzxrpmcn  43259  gsumge0cl  43799  ovnval2b  43980  volicorescl  43981  ovnsubaddlem1  43998