Theorem xrex 13025

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 11304	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11251	. . 3 ⊢ ℝ ∈ V
3		prex 5440	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7756	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2822	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2099  Vcvv 3462   ∪ cun 3945  {cpr 4635  ℝcr 11159  +∞cpnf 11297  -∞cmnf 11298  ℝ^*cxr 11299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5306  ax-nul 5313  ax-pr 5435  ax-un 7748  ax-cnex 11216  ax-resscn 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-sn 4634  df-pr 4636  df-uni 4916  df-xr 11304

This theorem is referenced by:  ixxval  13388  ixxf  13390  ixxex  13391  limsuple  15482  limsuplt  15483  limsupbnd1  15486  prdsds  17481  letsr  18620  xrsbas  21377  xrsadd  21378  xrsmul  21379  xrsle  21381  xrs1mnd  21403  xrs10  21404  xrs1cmn  21405  xrge0subm  21406  xrge0cmn  21407  xrsds  21408  znle  21532  leordtval2  23210  lecldbas  23217  ispsmet  24304  isxmet  24324  imasdsf1olem  24373  blfvalps  24383  nmoffn  24722  nmofval  24725  xrsxmet  24819  xrge0gsumle  24843  xrge0tsms  24844  xrlimcnp  26999  xrge00  32897  xrge0tsmsd  32928  xrhval  33835  ltex  41971  leex  41972  icof  44844  elicores  45169  fuzxrpmcn  45467  gsumge0cl  46010  ovnval2b  46191  volicorescl  46192  ovnsubaddlem1  46209