Theorem xrex 12385

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 10678	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 10627	. . 3 ⊢ ℝ ∈ V
3		prex 5332	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7468	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2909	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2110  Vcvv 3494   ∪ cun 3933  {cpr 4568  ℝcr 10535  +∞cpnf 10671  -∞cmnf 10672  ℝ^*cxr 10673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329  ax-un 7460  ax-cnex 10592  ax-resscn 10593

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-sn 4567  df-pr 4569  df-uni 4838  df-xr 10678

This theorem is referenced by:  ixxval  12745  ixxf  12747  ixxex  12748  limsuple  14834  limsuplt  14835  limsupbnd1  14838  prdsds  16736  letsr  17836  xrsbas  20560  xrsadd  20561  xrsmul  20562  xrsle  20564  xrs1mnd  20582  xrs10  20583  xrs1cmn  20584  xrge0subm  20585  xrge0cmn  20586  xrsds  20587  znle  20682  leordtval2  21819  lecldbas  21826  ispsmet  22913  isxmet  22933  imasdsf1olem  22982  blfvalps  22992  nmoffn  23319  nmofval  23322  xrsxmet  23416  xrge0gsumle  23440  xrge0tsms  23441  xrlimcnp  25545  xrge00  30673  xrge0tsmsd  30692  xrhval  31259  icof  41480  elicores  41807  fuzxrpmcn  42107  gsumge0cl  42652  ovnval2b  42833  volicorescl  42834  ovnsubaddlem1  42851