Theorem xrex 10980

Description: The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)

Assertion

Ref	Expression
xrex	|- RR* e. _V

Proof of Theorem xrex

Step	Hyp	Ref	Expression
1		df-xr 9414	. 2 |- RR* = ( RR u. { +oo , -oo } )
2		reex 9365	. . 3 |- RR e. _V
3		prex 4529	. . 3 |- { +oo , -oo } e. _V
4	2, 3	unex 6373	. 2 |- ( RR u. { +oo , -oo } ) e. _V
5	1, 4	eqeltri 2508	1 |- RR* e. _V

Syntax hints:   e. wcel 1756   _Vcvv 2967   u. cun 3321   {cpr 3874   RRcr 9273   +oocpnf 9407   -oocmnf 9408   RR*cxr 9409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-rex 2716  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-sn 3873  df-pr 3875  df-uni 4087  df-xr 9414

This theorem is referenced by:  ixxval  11300  ixxf  11302  ixxex  11303  limsuple  12948  limsuplt  12949  limsupbnd1  12952  prdsds  14394  letsr  15389  xrsbas  17807  xrsadd  17808  xrsmul  17809  xrsle  17811  xrs1mnd  17826  xrs10  17827  xrs1cmn  17828  xrge0subm  17829  xrge0cmn  17830  xrsds  17831  znle  17942  leordtval2  18791  lecldbas  18798  ispsmet  19855  isxmet  19874  imasdsf1olem  19923  blfvalps  19933  nmoffn  20265  nmofval  20268  xrsxmet  20361  xrge0gsumle  20385  xrge0tsms  20386  xrlimcnp  22337  xrge00  26098  xrge0tsmsd  26204  xrhval  26396