Theorem xrex 12240

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 10532	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 10481	. . 3 ⊢ ℝ ∈ V
3		prex 5231	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7333	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2881	1 ⊢ ℝ* ∈ V

Syntax hints:   ∈ wcel 2083  Vcvv 3440   ∪ cun 3863  {cpr 4480  ℝcr 10389  +∞cpnf 10525  -∞cmnf 10526  ℝ^*cxr 10527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228  ax-un 7326  ax-cnex 10446  ax-resscn 10447

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rex 3113  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-sn 4479  df-pr 4481  df-uni 4752  df-xr 10532

This theorem is referenced by:  ixxval  12600  ixxf  12602  ixxex  12603  limsuple  14673  limsuplt  14674  limsupbnd1  14677  prdsds  16570  letsr  17670  xrsbas  20247  xrsadd  20248  xrsmul  20249  xrsle  20251  xrs1mnd  20269  xrs10  20270  xrs1cmn  20271  xrge0subm  20272  xrge0cmn  20273  xrsds  20274  znle  20369  leordtval2  21508  lecldbas  21515  ispsmet  22601  isxmet  22621  imasdsf1olem  22670  blfvalps  22680  nmoffn  23007  nmofval  23010  xrsxmet  23104  xrge0gsumle  23128  xrge0tsms  23129  xrlimcnp  25232  xrge00  30343  xrge0tsmsd  30499  xrhval  30872  icof  41043  elicores  41372  fuzxrpmcn  41672  gsumge0cl  42217  ovnval2b  42398  volicorescl  42399  ovnsubaddlem1  42416