Theorem xrex 11102

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 9536	. 2 |- RR* = ( RR u. { +oo , -oo } )
2		reex 9487	. . 3 |- RR e. _V
3		prex 4645	. . 3 |- { +oo , -oo } e. _V
4	2, 3	unex 6491	. 2 |- ( RR u. { +oo , -oo } ) e. _V
5	1, 4	eqeltri 2538	1 |- RR* e. _V

Syntax hints:   e. wcel 1758   _Vcvv 3078   u. cun 3437   {cpr 3990   RRcr 9395   +oocpnf 9529   -oocmnf 9530   RR*cxr 9531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642  ax-un 6485  ax-cnex 9452  ax-resscn 9453

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rex 2805  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-sn 3989  df-pr 3991  df-uni 4203  df-xr 9536

This theorem is referenced by:  ixxval  11422  ixxf  11424  ixxex  11425  limsuple  13077  limsuplt  13078  limsupbnd1  13081  prdsds  14524  letsr  15519  xrsbas  17960  xrsadd  17961  xrsmul  17962  xrsle  17964  xrs1mnd  17979  xrs10  17980  xrs1cmn  17981  xrge0subm  17982  xrge0cmn  17983  xrsds  17984  znle  18095  leordtval2  18951  lecldbas  18958  ispsmet  20015  isxmet  20034  imasdsf1olem  20083  blfvalps  20093  nmoffn  20425  nmofval  20428  xrsxmet  20521  xrge0gsumle  20545  xrge0tsms  20546  xrlimcnp  22498  xrge00  26312  xrge0tsmsd  26418  xrhval  26609