Theorem xrex 12025

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 10332	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 10280	. . 3 ⊢ ℝ ∈ V
3		prex 5065	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7154	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2840	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2155  Vcvv 3350   ∪ cun 3730  {cpr 4336  ℝcr 10188  +∞cpnf 10325  -∞cmnf 10326  ℝ^*cxr 10327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rex 3061  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-sn 4335  df-pr 4337  df-uni 4595  df-xr 10332

This theorem is referenced by:  ixxval  12385  ixxf  12387  ixxex  12388  limsuple  14496  limsuplt  14497  limsupbnd1  14500  prdsds  16392  letsr  17495  xrsbas  20035  xrsadd  20036  xrsmul  20037  xrsle  20039  xrs1mnd  20057  xrs10  20058  xrs1cmn  20059  xrge0subm  20060  xrge0cmn  20061  xrsds  20062  znle  20157  leordtval2  21296  lecldbas  21303  ispsmet  22388  isxmet  22408  imasdsf1olem  22457  blfvalps  22467  nmoffn  22794  nmofval  22797  xrsxmet  22891  xrge0gsumle  22915  xrge0tsms  22916  xrlimcnp  24986  xrge00  30068  xrge0tsmsd  30167  xrhval  30444  icof  39988  elicores  40330  fuzxrpmcn  40624  gsumge0cl  41157  ovnval2b  41338  volicorescl  41339  ovnsubaddlem1  41356