Theorem xrex 11216

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 9631	. 2 |- RR* = ( RR u. { +oo , -oo } )
2		reex 9582	. . 3 |- RR e. _V
3		prex 4689	. . 3 |- { +oo , -oo } e. _V
4	2, 3	unex 6581	. 2 |- ( RR u. { +oo , -oo } ) e. _V
5	1, 4	eqeltri 2551	1 |- RR* e. _V

Syntax hints:   e. wcel 1767   _Vcvv 3113   u. cun 3474   {cpr 4029   RRcr 9490   +oocpnf 9624   -oocmnf 9625   RR*cxr 9626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686  ax-un 6575  ax-cnex 9547  ax-resscn 9548

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rex 2820  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-sn 4028  df-pr 4030  df-uni 4246  df-xr 9631

This theorem is referenced by:  ixxval  11536  ixxf  11538  ixxex  11539  limsuple  13263  limsuplt  13264  limsupbnd1  13267  prdsds  14718  letsr  15713  xrsbas  18221  xrsadd  18222  xrsmul  18223  xrsle  18225  xrs1mnd  18240  xrs10  18241  xrs1cmn  18242  xrge0subm  18243  xrge0cmn  18244  xrsds  18245  znle  18356  leordtval2  19495  lecldbas  19502  ispsmet  20559  isxmet  20578  imasdsf1olem  20627  blfvalps  20637  nmoffn  20969  nmofval  20972  xrsxmet  21065  xrge0gsumle  21089  xrge0tsms  21090  xrlimcnp  23042  xrge00  27352  xrge0tsmsd  27454  xrhval  27648