Theorem rexr 10029

Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
rexr	⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Proof of Theorem rexr

Step	Hyp	Ref	Expression
1		ressxr 10027	. 2 ⊢ ℝ ⊆ ℝ*
2	1	sseli 3579	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 1987  ℝcr 9879  ℝ^*cxr 10017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560  df-in 3562  df-ss 3569  df-xr 10022

This theorem is referenced by:  rexri  10041  lenlt  10060  ltpnf  11898  mnflt  11901  xrltnsym  11914  xrlttr  11917  xrre  11943  xrre3  11945  max1  11959  max2  11961  min1  11963  min2  11964  maxle  11965  lemin  11966  maxlt  11967  ltmin  11968  max0sub  11970  qbtwnxr  11974  xralrple  11979  alrple  11980  xltnegi  11990  rexadd  12006  xaddnemnf  12010  xaddnepnf  12011  xaddcom  12014  xnegdi  12021  xpncan  12024  xnpcan  12025  xleadd1a  12026  xleadd1  12028  xltadd1  12029  xltadd2  12030  xsubge0  12034  rexmul  12044  xadddilem  12067  xadddir  12069  xrsupsslem  12080  xrinfmsslem  12081  xrub  12085  supxrun  12089  supxrunb1  12092  supxrunb2  12093  supxrbnd1  12094  supxrbnd2  12095  xrsup0  12096  supxrbnd  12101  infmremnf  12115  elioo4g  12176  elioc2  12178  elico2  12179  elicc2  12180  iccss  12183  iooshf  12194  iooneg  12234  icoshft  12236  difreicc  12246  hashbnd  13063  elicc4abs  13993  icodiamlt  14108  limsupgord  14137  pcadd  15517  ramubcl  15646  lt6abl  18217  xrsmcmn  19688  xrs1mnd  19703  xrs10  19704  xrsdsreval  19710  psmetge0  22027  xmetge0  22059  imasdsf1olem  22088  bl2in  22115  blssps  22139  blss  22140  blcld  22220  icopnfcld  22481  iocmnfcld  22482  bl2ioo  22503  blssioo  22506  xrtgioo  22517  xrsblre  22522  iccntr  22532  icccmplem2  22534  icccmp  22536  reconnlem2  22538  xrge0tsms  22545  icoopnst  22646  iocopnst  22647  ovolfioo  23143  ovolicc2lem1  23192  ovolicc2lem5  23196  voliunlem3  23227  icombl1  23238  icombl  23239  iccvolcl  23242  ovolioo  23243  ioovolcl  23244  uniiccdif  23252  volsup2  23279  mbfimasn  23307  ismbf3d  23327  mbfsup  23337  itg2seq  23415  dvlip2  23662  ply1remlem  23826  abelthlem3  24091  abelth  24099  sincosq2sgn  24155  sincosq3sgn  24156  sinq12ge0  24164  sincos6thpi  24171  sineq0  24177  efif1olem1  24192  efif1olem2  24193  efif1o  24196  eff1o  24199  loglesqrt  24399  basellem1  24707  pntlemo  25196  nmobndi  27476  nmopub2tALT  28614  nmfnleub2  28631  nmopcoadji  28806  rexdiv  29416  xrge0tsmsd  29567  pnfneige0  29776  lmxrge0  29777  hashf2  29924  sxbrsigalem0  30111  omssubadd  30140  orvcgteel  30307  orvclteel  30312  sgnclre  30379  sgnneg  30380  signstfvneq0  30426  ivthALT  31969  icorempt2  32828  icoreunrn  32836  iooelexlt  32839  relowlssretop  32840  relowlpssretop  32841  poimir  33071  mblfinlem2  33076  iblabsnclem  33102  bddiblnc  33109  ftc1anclem1  33114  ftc1anclem6  33119  areacirclem5  33133  areacirc  33134  blbnd  33215  iocmbl  37276  supxrre3  39002  supxrgere  39010  infrpge  39028  infxrunb2  39045  infxrbnd2  39046  infleinflem2  39048  xrralrecnnle  39063  supxrunb3  39084  ioomidp  39148  limsupre  39274  limsupub  39337  limsuppnflem  39343  limsupre3lem  39365  icccncfext  39401  volioc  39492  volico  39504  fourierdlem113  39740  meaiuninclem  40001  icoresmbl  40061  ovolval5lem1  40170  mbfresmf  40252  cnfsmf  40253  incsmf  40255  smfconst  40262  decsmf  40279  smfres  40301  smfco  40313  issmfle2d  40319  bgoldbtbndlem3  40981