Theorem rexr 10687

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 10685	. 2 ⊢ ℝ ⊆ ℝ*
2	1	sseli 3963	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 10536  ℝ^*cxr 10674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-xr 10679

This theorem is referenced by:  rexri  10699  lenlt  10719  ltpnf  12516  mnflt  12519  xrltnsym  12531  xrlttr  12534  xrre  12563  xrre3  12565  max1  12579  max2  12581  min1  12583  min2  12584  maxle  12585  lemin  12586  maxlt  12587  ltmin  12588  max0sub  12590  qbtwnxr  12594  xralrple  12599  alrple  12600  xltnegi  12610  rexadd  12626  xaddnemnf  12630  xaddnepnf  12631  xaddcom  12634  xnegdi  12642  xpncan  12645  xnpcan  12646  xleadd1a  12647  xleadd1  12649  xltadd1  12650  xltadd2  12651  xsubge0  12655  rexmul  12665  xadddilem  12688  xadddir  12690  xrsupsslem  12701  xrinfmsslem  12702  xrub  12706  supxrun  12710  supxrunb1  12713  supxrunb2  12714  supxrbnd1  12715  supxrbnd2  12716  xrsup0  12717  supxrbnd  12722  infmremnf  12737  elioo4g  12798  elioc2  12800  elico2  12801  elicc2  12802  iccss  12805  iooshf  12816  iooneg  12858  icoshft  12860  difreicc  12871  hashbnd  13697  elicc4abs  14679  icodiamlt  14795  limsupgord  14829  pcadd  16225  ramubcl  16354  lt6abl  19015  xrsmcmn  20568  xrs1mnd  20583  xrs10  20584  xrsdsreval  20590  psmetge0  22922  xmetge0  22954  imasdsf1olem  22983  bl2in  23010  blssps  23034  blss  23035  blcld  23115  icopnfcld  23376  iocmnfcld  23377  bl2ioo  23400  blssioo  23403  xrtgioo  23414  xrsblre  23419  iccntr  23429  icccmplem2  23431  icccmp  23433  reconnlem2  23435  xrge0tsms  23442  icoopnst  23543  iocopnst  23544  ovolfioo  24068  ovolicc2lem1  24118  ovolicc2lem5  24122  voliunlem3  24153  icombl1  24164  icombl  24165  iccvolcl  24168  ovolioo  24169  ioovolcl  24171  uniiccdif  24179  volsup2  24206  mbfimasn  24233  ismbf3d  24255  mbfsup  24265  itg2seq  24343  dvlip2  24592  ply1remlem  24756  abelthlem3  25021  abelth  25029  sincosq2sgn  25085  sincosq3sgn  25086  sinq12ge0  25094  sincos6thpi  25101  sineq0  25109  efif1olem1  25126  efif1olem2  25127  efif1o  25130  eff1o  25133  loglesqrt  25339  basellem1  25658  pntlemo  26183  nmobndi  28552  nmopub2tALT  29686  nmfnleub2  29703  nmopcoadji  29878  rexdiv  30602  xrge0tsmsd  30692  pnfneige0  31194  lmxrge0  31195  hashf2  31343  sxbrsigalem0  31529  orvcgteel  31725  orvclteel  31730  sgnclre  31797  sgnneg  31798  signstfvn  31839  signstfvneq0  31842  signsvfn  31852  ivthALT  33683  icorempo  34635  icoreunrn  34643  iooelexlt  34646  relowlssretop  34647  relowlpssretop  34648  poimir  34940  mblfinlem2  34945  iblabsnclem  34970  bddiblnc  34977  ftc1anclem1  34982  ftc1anclem6  34987  areacirclem5  35001  areacirc  35002  blbnd  35080  iocmbl  39868  supxrre3  41642  supxrgere  41650  infrpge  41668  infxrunb2  41685  infxrbnd2  41686  infleinflem2  41688  xrralrecnnle  41702  supxrunb3  41721  supminfxr2  41794  xrpnf  41811  ioomidp  41839  limsupre  41971  limsupub  42034  limsuppnflem  42040  limsupre3lem  42062  liminfgord  42084  liminflelimsuplem  42105  limsupgtlem  42107  limsupub2  42142  xlimpnfxnegmnf  42144  xlimmnfvlem2  42163  xlimmnfv  42164  xlimpnfvlem2  42167  xlimpnfv  42168  icccncfext  42219  volioc  42306  volico  42317  fourierdlem113  42553  meaiuninclem  42811  meaiuninc3v  42815  icoresmbl  42874  ovolval5lem1  42983  mbfresmf  43065  cnfsmf  43066  incsmf  43068  smfconst  43075  decsmf  43092  smfres  43114  smfco  43126  issmfle2d  43132  bgoldbtbndlem3  44021  rrxsphere  44784