Theorem rexr 11382

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11226  ℝ^*cxr 11369

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-xr 11374

This theorem is used by:  rexri  11394  lenlt  11415  ltpnf  13276  mnflt  13279  xrltnsym  13293  xrlttr  13296  xrre  13326  xrre3  13328  max1  13342  max2  13344  min1  13346  min2  13347  maxle  13348  lemin  13349  maxlt  13350  ltmin  13351  max0sub  13353  qbtwnxr  13357  xralrple  13362  alrple  13363  xltnegi  13373  rexadd  13389  xaddnemnf  13393  xaddnepnf  13394  xaddcom  13397  xnegdi  13405  xpncan  13408  xnpcan  13409  xleadd1a  13410  xleadd1  13412  xltadd1  13413  xltadd2  13414  xsubge0  13418  rexmul  13428  xadddilem  13451  xadddir  13453  xrsupsslem  13464  xrinfmsslem  13465  xrub  13469  supxrun  13473  supxrunb1  13476  supxrunb2  13477  supxrbnd1  13478  supxrbnd2  13479  xrsup0  13480  supxrbnd  13485  infmremnf  13501  elioo4g  13564  elioc2  13567  elico2  13568  elicc2  13569  iccss  13572  iooshf  13584  iooneg  13629  icoshft  13631  difreicc  13642  hashbnd  14507  sgnneg  15282  sgnclre  15284  elicc4abs  15516  icodiamlt  15634  limsupgord  15668  pcadd  17096  ramubcl  17225  lt6abl  20139  xrsmcmn  21731  xrsdsreval  21748  xrs1mnd  21776  xrs10  21777  psmetge0  24661  xmetge0  24693  imasdsf1olem  24722  bl2in  24749  blssps  24773  blss  24774  blcld  24854  icopnfcld  25116  iocmnfcld  25117  bl2ioo  25141  blssioo  25144  xrtgioo  25156  xrsblre  25161  iccntr  25171  icccmplem2  25173  icccmp  25175  reconnlem2  25177  xrge0tsms  25184  icoopnst  25290  iocopnst  25291  ovolfioo  25818  ovolicc2lem1  25868  ovolicc2lem5  25872  voliunlem3  25903  icombl1  25914  icombl  25915  iccvolcl  25918  ovolioo  25919  ioovolcl  25921  uniiccdif  25929  volsup2  25956  mbfimasn  25983  ismbf3d  26005  mbfsup  26015  itg2seq  26093  bddiblnc  26192  dvlip2  26345  ply1remlem  26513  abelthlem3  26790  abelth  26798  sincosq2sgn  26858  sincosq3sgn  26859  sinq12ge0  26867  sincos6thpi  26874  sineq0  26882  efif1olem1  26900  efif1olem2  26901  efif1o  26904  eff1o  26907  loglesqrt  27119  basellem1  27438  pntlemo  27964  nmobndi  31407  nmopub2tALT  32541  nmfnleub2  32558  nmopcoadji  32733  rexdiv  33562  xrge0tsmsd  33704  pnfneige0  34653  lmxrge0  34654  hashf2  34786  sxbrsigalem0  34973  orvcgteel  35170  orvclteel  35175  signstfvn  35268  signstfvneq0  35271  signsvfn  35281  ivthALT  37301  icorempo  38466  icoreunrn  38474  iooelexlt  38477  relowlssretop  38478  relowlpssretop  38479  poimir  38763  mblfinlem2  38768  iblabsnclem  38793  ftc1anclem1  38803  ftc1anclem6  38808  areacirclem5  38822  areacirc  38823  blbnd  38913  iocmbl  44407  reabssgn  44828  supxrre3  46542  supxrgere  46550  infrpge  46568  infxrunb2  46584  infxrbnd2  46585  infleinflem2  46587  xrralrecnnle  46599  supxrunb3  46615  supminfxr2  46684  xrpnf  46700  ioomidp  46731  limsupre  46856  limsupub  46919  limsuppnflem  46925  limsupre3lem  46947  liminfgord  46969  liminflelimsuplem  46990  limsupgtlem  46992  limsupub2  47027  xlimpnfxnegmnf  47029  xlimmnfvlem2  47048  xlimmnfv  47049  xlimpnfvlem2  47052  xlimpnfv  47053  icccncfext  47102  volioc  47187  volico  47198  fourierdlem113  47434  meaiuninclem  47695  meaiuninc3v  47699  icoresmbl  47758  ovolval5lem1  47867  mbfresmf  47954  cnfsmf  47955  incsmf  47957  smfconst  47964  decsmf  47982  smfres  48005  smfco  48017  issmfle2d  48024  finfdm  48061  bgoldbtbndlem3  49110  rrxsphere  50065  i0oii  50239  io1ii  50240