Theorem rexr 11149

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 10996  ℝ^*cxr 11136

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3435  df-un 3904  df-ss 3916  df-xr 11141

This theorem is referenced by:  rexri  11161  lenlt  11182  ltpnf  13010  mnflt  13013  xrltnsym  13027  xrlttr  13030  xrre  13059  xrre3  13061  max1  13075  max2  13077  min1  13079  min2  13080  maxle  13081  lemin  13082  maxlt  13083  ltmin  13084  max0sub  13086  qbtwnxr  13090  xralrple  13095  alrple  13096  xltnegi  13106  rexadd  13122  xaddnemnf  13126  xaddnepnf  13127  xaddcom  13130  xnegdi  13138  xpncan  13141  xnpcan  13142  xleadd1a  13143  xleadd1  13145  xltadd1  13146  xltadd2  13147  xsubge0  13151  rexmul  13161  xadddilem  13184  xadddir  13186  xrsupsslem  13197  xrinfmsslem  13198  xrub  13202  supxrun  13206  supxrunb1  13209  supxrunb2  13210  supxrbnd1  13211  supxrbnd2  13212  xrsup0  13213  supxrbnd  13218  infmremnf  13234  elioo4g  13297  elioc2  13300  elico2  13301  elicc2  13302  iccss  13305  iooshf  13317  iooneg  13362  icoshft  13364  difreicc  13375  hashbnd  14231  elicc4abs  15214  icodiamlt  15332  limsupgord  15366  pcadd  16788  ramubcl  16917  lt6abl  19761  xrsmcmn  21282  xrsdsreval  21302  xrs1mnd  21331  xrs10  21332  psmetge0  24181  xmetge0  24213  imasdsf1olem  24242  bl2in  24269  blssps  24293  blss  24294  blcld  24374  icopnfcld  24636  iocmnfcld  24637  bl2ioo  24661  blssioo  24664  xrtgioo  24676  xrsblre  24681  iccntr  24691  icccmplem2  24693  icccmp  24695  reconnlem2  24697  xrge0tsms  24704  icoopnst  24817  iocopnst  24818  ovolfioo  25349  ovolicc2lem1  25399  ovolicc2lem5  25403  voliunlem3  25434  icombl1  25445  icombl  25446  iccvolcl  25449  ovolioo  25450  ioovolcl  25452  uniiccdif  25460  volsup2  25487  mbfimasn  25514  ismbf3d  25536  mbfsup  25546  itg2seq  25624  bddiblnc  25724  dvlip2  25881  ply1remlem  26051  abelthlem3  26324  abelth  26332  sincosq2sgn  26389  sincosq3sgn  26390  sinq12ge0  26398  sincos6thpi  26406  sineq0  26414  efif1olem1  26432  efif1olem2  26433  efif1o  26436  eff1o  26439  loglesqrt  26652  basellem1  26972  pntlemo  27499  nmobndi  30706  nmopub2tALT  31840  nmfnleub2  31857  nmopcoadji  32032  sgnclre  32770  sgnneg  32771  rexdiv  32861  xrge0tsmsd  33010  pnfneige0  33932  lmxrge0  33933  hashf2  34065  sxbrsigalem0  34252  orvcgteel  34449  orvclteel  34454  signstfvn  34550  signstfvneq0  34553  signsvfn  34563  ivthALT  36326  icorempo  37342  icoreunrn  37350  iooelexlt  37353  relowlssretop  37354  relowlpssretop  37355  poimir  37650  mblfinlem2  37655  iblabsnclem  37680  ftc1anclem1  37690  ftc1anclem6  37695  areacirclem5  37709  areacirc  37710  blbnd  37784  iocmbl  43203  reabssgn  43626  supxrre3  45321  supxrgere  45329  infrpge  45347  infxrunb2  45363  infxrbnd2  45364  infleinflem2  45366  xrralrecnnle  45378  supxrunb3  45394  supminfxr2  45464  xrpnf  45480  ioomidp  45511  limsupre  45636  limsupub  45699  limsuppnflem  45705  limsupre3lem  45727  liminfgord  45749  liminflelimsuplem  45770  limsupgtlem  45772  limsupub2  45807  xlimpnfxnegmnf  45809  xlimmnfvlem2  45828  xlimmnfv  45829  xlimpnfvlem2  45832  xlimpnfv  45833  icccncfext  45882  volioc  45967  volico  45978  fourierdlem113  46214  meaiuninclem  46475  meaiuninc3v  46479  icoresmbl  46538  ovolval5lem1  46647  mbfresmf  46734  cnfsmf  46735  incsmf  46737  smfconst  46744  decsmf  46762  smfres  46785  smfco  46797  issmfle2d  46804  finfdm  46841  bgoldbtbndlem3  47805  rrxsphere  48747  i0oii  48918  io1ii  48919