Theorem rexr 11279

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11126  ℝ^*cxr 11266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-xr 11271

This theorem is referenced by:  rexri  11291  lenlt  11311  ltpnf  13134  mnflt  13137  xrltnsym  13151  xrlttr  13154  xrre  13183  xrre3  13185  max1  13199  max2  13201  min1  13203  min2  13204  maxle  13205  lemin  13206  maxlt  13207  ltmin  13208  max0sub  13210  qbtwnxr  13214  xralrple  13219  alrple  13220  xltnegi  13230  rexadd  13246  xaddnemnf  13250  xaddnepnf  13251  xaddcom  13254  xnegdi  13262  xpncan  13265  xnpcan  13266  xleadd1a  13267  xleadd1  13269  xltadd1  13270  xltadd2  13271  xsubge0  13275  rexmul  13285  xadddilem  13308  xadddir  13310  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  supxrun  13330  supxrunb1  13333  supxrunb2  13334  supxrbnd1  13335  supxrbnd2  13336  xrsup0  13337  supxrbnd  13342  infmremnf  13358  elioo4g  13421  elioc2  13424  elico2  13425  elicc2  13426  iccss  13429  iooshf  13441  iooneg  13486  icoshft  13488  difreicc  13499  hashbnd  14352  elicc4abs  15336  icodiamlt  15452  limsupgord  15486  pcadd  16907  ramubcl  17036  lt6abl  19874  xrsmcmn  21352  xrs1mnd  21370  xrs10  21371  xrsdsreval  21377  psmetge0  24249  xmetge0  24281  imasdsf1olem  24310  bl2in  24337  blssps  24361  blss  24362  blcld  24442  icopnfcld  24704  iocmnfcld  24705  bl2ioo  24729  blssioo  24732  xrtgioo  24744  xrsblre  24749  iccntr  24759  icccmplem2  24761  icccmp  24763  reconnlem2  24765  xrge0tsms  24772  icoopnst  24885  iocopnst  24886  ovolfioo  25418  ovolicc2lem1  25468  ovolicc2lem5  25472  voliunlem3  25503  icombl1  25514  icombl  25515  iccvolcl  25518  ovolioo  25519  ioovolcl  25521  uniiccdif  25529  volsup2  25556  mbfimasn  25583  ismbf3d  25605  mbfsup  25615  itg2seq  25693  bddiblnc  25793  dvlip2  25950  ply1remlem  26120  abelthlem3  26393  abelth  26401  sincosq2sgn  26458  sincosq3sgn  26459  sinq12ge0  26467  sincos6thpi  26475  sineq0  26483  efif1olem1  26501  efif1olem2  26502  efif1o  26505  eff1o  26508  loglesqrt  26721  basellem1  27041  pntlemo  27568  nmobndi  30702  nmopub2tALT  31836  nmfnleub2  31853  nmopcoadji  32028  sgnclre  32757  sgnneg  32758  rexdiv  32846  xrge0tsmsd  33002  pnfneige0  33928  lmxrge0  33929  hashf2  34061  sxbrsigalem0  34249  orvcgteel  34446  orvclteel  34451  signstfvn  34547  signstfvneq0  34550  signsvfn  34560  ivthALT  36299  icorempo  37315  icoreunrn  37323  iooelexlt  37326  relowlssretop  37327  relowlpssretop  37328  poimir  37623  mblfinlem2  37628  iblabsnclem  37653  ftc1anclem1  37663  ftc1anclem6  37668  areacirclem5  37682  areacirc  37683  blbnd  37757  iocmbl  43184  reabssgn  43607  supxrre3  45300  supxrgere  45308  infrpge  45326  infxrunb2  45343  infxrbnd2  45344  infleinflem2  45346  xrralrecnnle  45358  supxrunb3  45374  supminfxr2  45444  xrpnf  45460  ioomidp  45491  limsupre  45618  limsupub  45681  limsuppnflem  45687  limsupre3lem  45709  liminfgord  45731  liminflelimsuplem  45752  limsupgtlem  45754  limsupub2  45789  xlimpnfxnegmnf  45791  xlimmnfvlem2  45810  xlimmnfv  45811  xlimpnfvlem2  45814  xlimpnfv  45815  icccncfext  45864  volioc  45949  volico  45960  fourierdlem113  46196  meaiuninclem  46457  meaiuninc3v  46461  icoresmbl  46520  ovolval5lem1  46629  mbfresmf  46716  cnfsmf  46717  incsmf  46719  smfconst  46726  decsmf  46744  smfres  46767  smfco  46779  issmfle2d  46786  finfdm  46823  bgoldbtbndlem3  47769  rrxsphere  48676  i0oii  48842  io1ii  48843