Theorem rexr 11336

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11180  ℝ^*cxr 11323

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-xr 11328

This theorem is used by:  rexri  11348  lenlt  11369  ltpnf  13230  mnflt  13233  xrltnsym  13247  xrlttr  13250  xrre  13280  xrre3  13282  max1  13296  max2  13298  min1  13300  min2  13301  maxle  13302  lemin  13303  maxlt  13304  ltmin  13305  max0sub  13307  qbtwnxr  13311  xralrple  13316  alrple  13317  xltnegi  13327  rexadd  13343  xaddnemnf  13347  xaddnepnf  13348  xaddcom  13351  xnegdi  13359  xpncan  13362  xnpcan  13363  xleadd1a  13364  xleadd1  13366  xltadd1  13367  xltadd2  13368  xsubge0  13372  rexmul  13382  xadddilem  13405  xadddir  13407  xrsupsslem  13418  xrinfmsslem  13419  xrub  13423  supxrun  13427  supxrunb1  13430  supxrunb2  13431  supxrbnd1  13432  supxrbnd2  13433  xrsup0  13434  supxrbnd  13439  infmremnf  13455  elioo4g  13518  elioc2  13521  elico2  13522  elicc2  13523  iccss  13526  iooshf  13538  iooneg  13583  icoshft  13585  difreicc  13596  hashbnd  14460  sgnneg  15233  sgnclre  15235  elicc4abs  15467  icodiamlt  15585  limsupgord  15619  pcadd  17047  ramubcl  17176  lt6abl  20089  xrsmcmn  21681  xrsdsreval  21698  xrs1mnd  21726  xrs10  21727  psmetge0  24611  xmetge0  24643  imasdsf1olem  24672  bl2in  24699  blssps  24723  blss  24724  blcld  24804  icopnfcld  25066  iocmnfcld  25067  bl2ioo  25091  blssioo  25094  xrtgioo  25106  xrsblre  25111  iccntr  25121  icccmplem2  25123  icccmp  25125  reconnlem2  25127  xrge0tsms  25134  icoopnst  25240  iocopnst  25241  ovolfioo  25768  ovolicc2lem1  25818  ovolicc2lem5  25822  voliunlem3  25853  icombl1  25864  icombl  25865  iccvolcl  25868  ovolioo  25869  ioovolcl  25871  uniiccdif  25879  volsup2  25906  mbfimasn  25933  ismbf3d  25955  mbfsup  25965  itg2seq  26043  bddiblnc  26142  dvlip2  26295  ply1remlem  26463  abelthlem3  26742  abelth  26750  sincosq2sgn  26810  sincosq3sgn  26811  sinq12ge0  26819  sincos6thpi  26826  sineq0  26834  efif1olem1  26852  efif1olem2  26853  efif1o  26856  eff1o  26859  loglesqrt  27071  basellem1  27390  pntlemo  27916  nmobndi  31359  nmopub2tALT  32493  nmfnleub2  32510  nmopcoadji  32685  rexdiv  33474  xrge0tsmsd  33616  pnfneige0  34565  lmxrge0  34566  hashf2  34698  sxbrsigalem0  34886  orvcgteel  35083  orvclteel  35088  signstfvn  35181  signstfvneq0  35184  signsvfn  35194  ivthALT  37093  icorempo  38242  icoreunrn  38250  iooelexlt  38253  relowlssretop  38254  relowlpssretop  38255  poimir  38539  mblfinlem2  38544  iblabsnclem  38569  ftc1anclem1  38579  ftc1anclem6  38584  areacirclem5  38598  areacirc  38599  blbnd  38689  iocmbl  44173  reabssgn  44595  supxrre3  46281  supxrgere  46289  infrpge  46307  infxrunb2  46323  infxrbnd2  46324  infleinflem2  46326  xrralrecnnle  46338  supxrunb3  46354  supminfxr2  46423  xrpnf  46439  ioomidp  46470  limsupre  46595  limsupub  46658  limsuppnflem  46664  limsupre3lem  46686  liminfgord  46708  liminflelimsuplem  46729  limsupgtlem  46731  limsupub2  46766  xlimpnfxnegmnf  46768  xlimmnfvlem2  46787  xlimmnfv  46788  xlimpnfvlem2  46791  xlimpnfv  46792  icccncfext  46841  volioc  46926  volico  46937  fourierdlem113  47173  meaiuninclem  47434  meaiuninc3v  47438  icoresmbl  47497  ovolval5lem1  47606  mbfresmf  47693  cnfsmf  47694  incsmf  47696  smfconst  47703  decsmf  47721  smfres  47744  smfco  47756  issmfle2d  47763  finfdm  47800  bgoldbtbndlem3  48849  rrxsphere  49804  i0oii  49972  io1ii  49973