Theorem ressxr 9962

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 3738	. 2 ⊢ ℝ ⊆ (ℝ ∪ {+∞, -∞})
2		df-xr 9957	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
3	1, 2	sseqtr4i 3601	1 ⊢ ℝ ⊆ ℝ*

Syntax hints:   ∪ cun 3538   ⊆ wss 3540  {cpr 4127  ℝcr 9814  +∞cpnf 9950  -∞cmnf 9951  ℝ^*cxr 9952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-xr 9957

This theorem is referenced by:  rexpssxrxp  9963  rexr  9964  0xr  9965  rexrd  9968  ltrelxr  9978  supxrre  12029  supxrbnd  12030  supxrgtmnf  12031  supxrre1  12032  supxrre2  12033  infxrre  12038  iooval2  12079  fzval2  12200  uzsup  12524  hashxrcl  13010  seqcoll  13105  limsupval2  14059  limsupgre  14060  limsupbnd2  14062  rlimuni  14129  rlimcld2  14157  rlimno1  14232  isercolllem2  14244  isercoll  14246  caucvgrlem  14251  summolem2a  14293  prodmolem2a  14503  ramtlecl  15542  ramxrcl  15559  ismet2  21948  prdsmet  21985  qtopbas  22373  tgqioo  22411  re2ndc  22412  xrsmopn  22423  metdcn2  22450  metdscn2  22468  bndth  22565  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliun  23080  ovolicc2lem4  23095  voliunlem2  23126  voliunlem3  23127  opnmblALT  23177  vitalilem4  23186  mbfimaopnlem  23228  itg2le  23312  itg2seq  23315  dvfsumrlim  23598  itgsubst  23616  mdegleb  23628  mdeglt  23629  mdegldg  23630  mdegxrcl  23631  mdegcl  23633  mdegaddle  23638  mdegmullem  23642  deg1mul3le  23680  ig1pdvds  23740  aannenlem2  23888  taylfval  23917  radcnvcl  23975  radcnvlt1  23976  radcnvle  23978  xrlimcnp  24495  nmoxr  27005  nmooge0  27006  nmoolb  27010  nmoubi  27011  nmlno0lem  27032  nmopxr  28109  nmfnxr  28122  nmoplb  28150  nmopub  28151  nmfnlb  28167  nmfnleub  28168  nmlnop0iALT  28238  nmopun  28257  branmfn  28348  pjnmopi  28391  xlt2addrd  28913  xreceu  28961  rexdiv  28965  xrsmulgzz  29009  esumcst  29452  icorempt2  32375  mblfinlem2  32617  itg2addnc  32634  prdsbnd  32762  rrnequiv  32804  hbtlem2  36713  binomcxplemdvbinom  37574  binomcxplemcvg  37575  binomcxplemnotnn0  37577  suplesup  38496  frexr  38545  elicores  38607  ressiocsup  38628  ressioosup  38629  ressiooinf  38631  limsupre  38708  volicoff  38888  volicofmpt  38890  fourierdlem52  39051  fourierdlem103  39102  fourierdlem104  39103  etransclem48  39175  ioorrnopnlem  39200  fsumlesge0  39270  sge0cl  39274  sge0supre  39282  sge0less  39285  sge0split  39302  sge0seq  39339  hoicvr  39438  volicorescl  39443  ovolval2lem  39533  ovolval5lem2  39543  ovnovollem1  39546  ovnovollem2  39547  iinhoiicclem  39564  iunhoiioolem  39566  iccvonmbllem  39569  vonioolem2  39572  vonioo  39573  vonicclem2  39575  vonicc  39576  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605