Theorem xrex 12807

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 11093	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11042	. . 3 ⊢ ℝ ∈ V
3		prex 5370	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7638	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2834	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2105  Vcvv 3441   ∪ cun 3895  {cpr 4573  ℝcr 10950  +∞cpnf 11086  -∞cmnf 11087  ℝ^*cxr 11088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367  ax-un 7630  ax-cnex 11007  ax-resscn 11008

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-sn 4572  df-pr 4574  df-uni 4851  df-xr 11093

This theorem is referenced by:  ixxval  13167  ixxf  13169  ixxex  13170  limsuple  15266  limsuplt  15267  limsupbnd1  15270  prdsds  17252  letsr  18388  xrsbas  20697  xrsadd  20698  xrsmul  20699  xrsle  20701  xrs1mnd  20719  xrs10  20720  xrs1cmn  20721  xrge0subm  20722  xrge0cmn  20723  xrsds  20724  znle  20823  leordtval2  22446  lecldbas  22453  ispsmet  23540  isxmet  23560  imasdsf1olem  23609  blfvalps  23619  nmoffn  23958  nmofval  23961  xrsxmet  24055  xrge0gsumle  24079  xrge0tsms  24080  xrlimcnp  26201  xrge00  31430  xrge0tsmsd  31452  xrhval  32108  icof  43000  elicores  43321  fuzxrpmcn  43619  gsumge0cl  44160  ovnval2b  44341  volicorescl  44342  ovnsubaddlem1  44359