Theorem rexr 11283

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-xr 11275

This theorem is used by:  rexri  11295  lenlt  11316  ltpnf  13175  mnflt  13178  xrltnsym  13192  xrlttr  13195  xrre  13225  xrre3  13227  max1  13241  max2  13243  min1  13245  min2  13246  maxle  13247  lemin  13248  maxlt  13249  ltmin  13250  max0sub  13252  qbtwnxr  13256  xralrple  13261  alrple  13262  xltnegi  13272  rexadd  13288  xaddnemnf  13292  xaddnepnf  13293  xaddcom  13296  xnegdi  13304  xpncan  13307  xnpcan  13308  xleadd1a  13309  xleadd1  13311  xltadd1  13312  xltadd2  13313  xsubge0  13317  rexmul  13327  xadddilem  13350  xadddir  13352  xrsupsslem  13363  xrinfmsslem  13364  xrub  13368  supxrun  13372  supxrunb1  13375  supxrunb2  13376  supxrbnd1  13377  supxrbnd2  13378  xrsup0  13379  supxrbnd  13384  infmremnf  13400  elioo4g  13463  elioc2  13466  elico2  13467  elicc2  13468  iccss  13471  iooshf  13483  iooneg  13528  icoshft  13530  difreicc  13541  hashbnd  14404  sgnneg  15177  sgnclre  15179  elicc4abs  15411  icodiamlt  15529  limsupgord  15563  pcadd  16987  ramubcl  17116  lt6abl  20028  xrsmcmn  21614  xrsdsreval  21631  xrs1mnd  21659  xrs10  21660  psmetge0  24544  xmetge0  24576  imasdsf1olem  24605  bl2in  24632  blssps  24656  blss  24657  blcld  24737  icopnfcld  24999  iocmnfcld  25000  bl2ioo  25024  blssioo  25027  xrtgioo  25039  xrsblre  25044  iccntr  25054  icccmplem2  25056  icccmp  25058  reconnlem2  25060  xrge0tsms  25067  icoopnst  25173  iocopnst  25174  ovolfioo  25701  ovolicc2lem1  25751  ovolicc2lem5  25755  voliunlem3  25786  icombl1  25797  icombl  25798  iccvolcl  25801  ovolioo  25802  ioovolcl  25804  uniiccdif  25812  volsup2  25839  mbfimasn  25866  ismbf3d  25888  mbfsup  25898  itg2seq  25976  bddiblnc  26076  dvlip2  26229  ply1remlem  26397  abelthlem3  26676  abelth  26684  sincosq2sgn  26744  sincosq3sgn  26745  sinq12ge0  26753  sincos6thpi  26761  sineq0  26769  efif1olem1  26787  efif1olem2  26788  efif1o  26791  eff1o  26794  loglesqrt  27006  basellem1  27325  pntlemo  27851  nmobndi  31264  nmopub2tALT  32398  nmfnleub2  32415  nmopcoadji  32590  rexdiv  33379  xrge0tsmsd  33521  pnfneige0  34469  lmxrge0  34470  hashf2  34602  sxbrsigalem0  34790  orvcgteel  34987  orvclteel  34992  signstfvn  35085  signstfvneq0  35088  signsvfn  35098  ivthALT  36962  icorempo  38113  icoreunrn  38121  iooelexlt  38124  relowlssretop  38125  relowlpssretop  38126  poimir  38410  mblfinlem2  38415  iblabsnclem  38440  ftc1anclem1  38450  ftc1anclem6  38455  areacirclem5  38469  areacirc  38470  blbnd  38545  iocmbl  44062  reabssgn  44484  supxrre3  46163  supxrgere  46171  infrpge  46189  infxrunb2  46205  infxrbnd2  46206  infleinflem2  46208  xrralrecnnle  46220  supxrunb3  46236  supminfxr2  46305  xrpnf  46321  ioomidp  46352  limsupre  46477  limsupub  46540  limsuppnflem  46546  limsupre3lem  46568  liminfgord  46590  liminflelimsuplem  46611  limsupgtlem  46613  limsupub2  46648  xlimpnfxnegmnf  46650  xlimmnfvlem2  46669  xlimmnfv  46670  xlimpnfvlem2  46673  xlimpnfv  46674  icccncfext  46723  volioc  46808  volico  46819  fourierdlem113  47055  meaiuninclem  47316  meaiuninc3v  47320  icoresmbl  47379  ovolval5lem1  47488  mbfresmf  47575  cnfsmf  47576  incsmf  47578  smfconst  47585  decsmf  47603  smfres  47626  smfco  47638  issmfle2d  47645  finfdm  47682  bgoldbtbndlem3  48731  rrxsphere  49686  i0oii  49854  io1ii  49855