Theorem rexr 10364

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

Syntax hints:   → wi 4   ∈ wcel 2155  ℝcr 10214  ℝ^*cxr 10352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-v 3389  df-un 3768  df-in 3770  df-ss 3777  df-xr 10357

This theorem is referenced by:  rexri  10376  lenlt  10395  ltpnf  12164  mnflt  12167  xrltnsym  12180  xrlttr  12183  xrre  12212  xrre3  12214  max1  12228  max2  12230  min1  12232  min2  12233  maxle  12234  lemin  12235  maxlt  12236  ltmin  12237  max0sub  12239  qbtwnxr  12243  xralrple  12248  alrple  12249  xltnegi  12259  rexadd  12275  xaddnemnf  12279  xaddnepnf  12280  xaddcom  12283  xnegdi  12290  xpncan  12293  xnpcan  12294  xleadd1a  12295  xleadd1  12297  xltadd1  12298  xltadd2  12299  xsubge0  12303  rexmul  12313  xadddilem  12336  xadddir  12338  xrsupsslem  12349  xrinfmsslem  12350  xrub  12354  supxrun  12358  supxrunb1  12361  supxrunb2  12362  supxrbnd1  12363  supxrbnd2  12364  xrsup0  12365  supxrbnd  12370  infmremnf  12385  elioo4g  12446  elioc2  12448  elico2  12449  elicc2  12450  iccss  12453  iooshf  12464  iooneg  12507  icoshft  12509  difreicc  12521  hashbnd  13337  elicc4abs  14276  icodiamlt  14391  limsupgord  14420  pcadd  15804  ramubcl  15933  lt6abl  18491  xrsmcmn  19971  xrs1mnd  19986  xrs10  19987  xrsdsreval  19993  psmetge0  22324  xmetge0  22356  imasdsf1olem  22385  bl2in  22412  blssps  22436  blss  22437  blcld  22517  icopnfcld  22778  iocmnfcld  22779  bl2ioo  22802  blssioo  22805  xrtgioo  22816  xrsblre  22821  iccntr  22831  icccmplem2  22833  icccmp  22835  reconnlem2  22837  xrge0tsms  22844  icoopnst  22945  iocopnst  22946  ovolfioo  23442  ovolicc2lem1  23492  ovolicc2lem5  23496  voliunlem3  23527  icombl1  23538  icombl  23539  iccvolcl  23542  ovolioo  23543  ioovolcl  23545  uniiccdif  23553  volsup2  23580  mbfimasn  23607  ismbf3d  23629  mbfsup  23639  itg2seq  23717  dvlip2  23966  ply1remlem  24130  abelthlem3  24395  abelth  24403  sincosq2sgn  24460  sincosq3sgn  24461  sinq12ge0  24469  sincos6thpi  24476  sineq0  24482  efif1olem1  24497  efif1olem2  24498  efif1o  24501  eff1o  24504  loglesqrt  24707  basellem1  25015  pntlemo  25504  nmobndi  27952  nmopub2tALT  29090  nmfnleub2  29107  nmopcoadji  29282  rexdiv  29953  xrge0tsmsd  30104  pnfneige0  30316  lmxrge0  30317  hashf2  30465  sxbrsigalem0  30652  omssubadd  30681  orvcgteel  30848  orvclteel  30853  sgnclre  30920  sgnneg  30921  signstfvneq0  30968  ivthALT  32645  icorempt2  33509  icoreunrn  33517  iooelexlt  33520  relowlssretop  33521  relowlpssretop  33522  poimir  33749  mblfinlem2  33754  iblabsnclem  33779  bddiblnc  33786  ftc1anclem1  33791  ftc1anclem6  33796  areacirclem5  33810  areacirc  33811  blbnd  33891  iocmbl  38292  supxrre3  40015  supxrgere  40023  infrpge  40041  infxrunb2  40058  infxrbnd2  40059  infleinflem2  40061  xrralrecnnle  40076  supxrunb3  40096  supminfxr2  40172  xrpnf  40189  ioomidp  40215  limsupre  40347  limsupub  40410  limsuppnflem  40416  limsupre3lem  40438  liminfgord  40460  liminflelimsuplem  40481  limsupgtlem  40483  xlimmnfvlem2  40533  xlimmnfv  40534  xlimpnfvlem2  40537  xlimpnfv  40538  icccncfext  40574  volioc  40661  volico  40673  fourierdlem113  40909  meaiuninclem  41170  meaiuninc3v  41174  icoresmbl  41233  ovolval5lem1  41342  mbfresmf  41424  cnfsmf  41425  incsmf  41427  smfconst  41434  decsmf  41451  smfres  41473  smfco  41485  issmfle2d  41491  bgoldbtbndlem3  42264