Theorem ressxr 11281

Description: The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
ressxr	⊢ ℝ ⊆ ℝ*

Proof of Theorem ressxr

Step	Hyp	Ref	Expression
1		ssun1 4127	. 2 ⊢ ℝ ⊆ (ℝ ∪ {+∞, -∞})
2		df-xr 11275	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
3	1, 2	sseqtrri 3983	1 ⊢ ℝ ⊆ ℝ*

This proof depends on syntax axioms:   ∪ cun 3900   ⊆ wss 3902  {cpr 4589  ℝcr 11127  +∞cpnf 11268  -∞cmnf 11269  ℝ^*cxr 11270

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-xr 11275

This theorem is used by:  rexpssxrxp  11282  rexr  11283  0xr  11284  rexrd  11287  ltrelxr  11298  supxrre  13383  supxrbnd  13384  supxrgtmnf  13385  supxrre1  13386  supxrre2  13387  infxrre  13393  iooval2  13435  fzval2  13568  uzsup  13928  hashxrcl  14425  seqcoll  14533  limsupval2  15571  limsupgre  15572  limsupbnd2  15574  rlimuni  15641  rlimcld2  15669  rlimno1  15745  isercolllem2  15757  isercoll  15759  caucvgrlem  15764  summolem2a  15805  prodmolem2a  16027  ramtlecl  17098  ramxrcl  17115  ismet2  24565  prdsmet  24602  qtopbas  24991  tgqioo  25032  re2ndc  25033  xrsmopn  25045  metdcn2  25072  metdscn2  25090  bndth  25192  ovolunlem1a  25730  ovolunlem1  25731  ovoliunlem1  25736  ovoliun  25739  ovolicc2lem4  25754  voliunlem2  25785  voliunlem3  25786  opnmblALT  25837  vitalilem4  25845  mbfimaopnlem  25889  itg2le  25973  itg2seq  25976  dvfsumrlim  26265  itgsubst  26283  mdegleb  26296  mdeglt  26297  mdegldg  26298  mdegxrcl  26299  mdegcl  26301  mdegaddle  26306  mdegmullem  26310  deg1mul3le  26349  ig1pdvds  26412  aannenlem2  26572  taylfval  26602  radcnvcl  26660  radcnvlt1  26661  radcnvle  26663  xrlimcnp  27213  nmoxr  31255  nmooge0  31256  nmoolb  31260  nmoubi  31261  nmlno0lem  31282  nmopxr  32355  nmfnxr  32368  nmoplb  32396  nmopub  32397  nmfnlb  32413  nmfnleub  32414  nmlnop0iALT  32484  nmopun  32503  branmfn  32594  pjnmopi  32637  xlt2addrd  33238  xreceu  33375  rexdiv  33379  xrsmulgzz  33457  esumcst  34581  icorempo  38113  mblfinlem2  38415  itg2addnc  38431  prdsbnd  38551  rrnequiv  38593  hbtlem2  43973  binomcxplemdvbinom  45185  binomcxplemcvg  45186  binomcxplemnotnn0  45188  suplesup  46177  frexr  46222  zssxr  46234  ssrexr  46268  uzxrd  46298  supminfxr  46300  rpssxr  46316  elicores  46371  ressiocsup  46392  ressioosup  46393  ressiooinf  46395  uzinico  46397  limsupre  46477  limsupresico  46536  limsupmnflem  46556  supcnvlimsup  46576  liminfresico  46607  volicoff  46831  volicofmpt  46833  fourierdlem52  46994  fourierdlem103  47045  fourierdlem104  47046  etransclem48  47118  ioorrnopnlem  47140  fsumlesge0  47213  sge0cl  47217  sge0supre  47225  sge0less  47228  sge0split  47245  sge0seq  47282  volicorescl  47389  ovolval2lem  47479  ovolval5lem2  47489  ovnovollem1  47492  ovnovollem2  47493  iinhoiicclem  47509  iunhoiioolem  47511  iccvonmbllem  47514  vonioolem2  47517  vonioo  47518  vonicclem2  47520  vonicc  47521  pimdecfgtioc  47551  pimincfltioc  47552  pimdecfgtioo  47553  pimincfltioo  47554  smflimsuplem4  47659