Theorem xrex 13029

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 11299	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11246	. . 3 ⊢ ℝ ∈ V
3		prex 5437	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7764	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2837	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3480   ∪ cun 3949  {cpr 4628  ℝcr 11154  +∞cpnf 11292  -∞cmnf 11293  ℝ^*cxr 11294

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-sn 4627  df-pr 4629  df-uni 4908  df-xr 11299

This theorem is referenced by:  ixxval  13395  ixxf  13397  ixxex  13398  limsuple  15514  limsuplt  15515  limsupbnd1  15518  prdsds  17509  letsr  18638  xrsbas  21396  xrsadd  21397  xrsmul  21398  xrsle  21400  xrs1mnd  21422  xrs10  21423  xrs1cmn  21424  xrge0subm  21425  xrge0cmn  21426  xrsds  21427  znle  21551  leordtval2  23220  lecldbas  23227  ispsmet  24314  isxmet  24334  imasdsf1olem  24383  blfvalps  24393  nmoffn  24732  nmofval  24735  xrsxmet  24831  xrge0gsumle  24855  xrge0tsms  24856  xrlimcnp  27011  xrge00  33017  xrge0tsmsd  33065  xrhval  34019  ltex  42286  leex  42287  icof  45224  elicores  45546  fuzxrpmcn  45843  gsumge0cl  46386  ovnval2b  46567  volicorescl  46568  ovnsubaddlem1  46585