Theorem xrex 10565

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 9080	. 2 |- RR* = ( RR u. { +oo , -oo } )
2		reex 9037	. . 3 |- RR e. _V
3		prex 4366	. . 3 |- { +oo , -oo } e. _V
4	2, 3	unex 4666	. 2 |- ( RR u. { +oo , -oo } ) e. _V
5	1, 4	eqeltri 2474	1 |- RR* e. _V

Syntax hints:   e. wcel 1721   _Vcvv 2916   u. cun 3278   {cpr 3775   RRcr 8945   +oocpnf 9073   -oocmnf 9074   RR*cxr 9075

This theorem is referenced by:  ixxval  10880  ixxf  10882  ixxex  10883  limsuple  12227  limsuplt  12228  limsupbnd1  12231  prdsds  13641  letsr  14627  xrsbas  16672  xrsadd  16673  xrsmul  16674  xrsle  16676  xrs1mnd  16691  xrs10  16692  xrs1cmn  16693  xrge0subm  16694  xrge0cmn  16695  xrsds  16696  znle  16772  leordtval2  17230  lecldbas  17237  ispsmet  18288  isxmet  18307  imasdsf1olem  18356  blfvalps  18366  nmoffn  18698  nmofval  18701  xrsxmet  18793  xrge0gsumle  18817  xrge0tsms  18818  xrlimcnp  20760  xrge00  24161  xrge0tsmsd  24176  xrhval  24337

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-rex 2672  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-sn 3780  df-pr 3781  df-uni 3976  df-xr 9080