Theorem rexrd 11184

Description: A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rexrd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
rexrd	⊢ (𝜑 → 𝐴 ∈ ℝ*)

Proof of Theorem rexrd

Step	Hyp	Ref	Expression
1		ressxr 11178	. 2 ⊢ ℝ ⊆ ℝ*
2		rexrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1, 2	sselid 3935	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11027  ℝ^*cxr 11167

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 3440  df-un 3910  df-ss 3922  df-xr 11172

This theorem is referenced by:  xnn0xr  12480  rpxr  12921  rpxrd  12956  max0sub  13116  qextltlem  13122  xralrple  13125  xnegcl  13133  xaddf  13144  xnn0lem1lt  13164  xnn0lenn0nn0  13165  xmulf  13192  xadddi  13215  xrub  13232  supxrre  13247  infxrre  13257  ixxub  13287  ixxlb  13288  ioo0  13291  ico0  13312  ioc0  13313  iooshf  13347  icoshftf1o  13395  supicc  13422  supiccub  13423  supicclub  13424  xnn0xrge0  13427  ssfzunsn  13491  addmodid  13844  hashnnn0genn0  14268  hashunsnggt  14319  elicc4abs  15245  caucvgrlem  15598  fprodge1  15920  pcxcl  16791  pcdvdsb  16799  pcaddlem  16818  ramcl2lem  16939  ramlb  16949  0ram  16950  setsstruct  17105  prdsxmetlem  24272  xblss2ps  24305  xblss2  24306  blss2ps  24307  blss2  24308  blhalf  24309  metustto  24457  metustexhalf  24460  nmoi  24632  nmoix  24633  nmoi2  24634  nmoleub  24635  qdensere  24673  cnblcld  24678  ioo2blex  24698  tgioo  24700  blcvx  24702  zcld  24718  recld2  24719  iccntr  24726  icccmplem1  24727  reconnlem1  24731  reconnlem2  24732  opnreen  24736  metnrmlem3  24766  icoopnst  24852  iocopnst  24853  cnheibor  24870  lebnumii  24881  nmoleub2lem  25030  lmnn  25179  iscau3  25194  minveclem4  25348  ivthlem1  25368  ivthlem2  25369  ivthlem3  25370  ivth2  25372  ivthle  25373  ivthle2  25374  ivthicc  25375  evthicc  25376  cniccbdd  25378  ovolgelb  25397  ovollb2lem  25405  ovolunlem1  25414  ovoliunlem1  25419  ovoliunlem2  25420  ovoliun  25422  ovolscalem1  25430  ovolicc1  25433  ovolicc2lem4  25437  ovolicc2lem5  25438  ovolicc2  25439  ovolicc  25440  nulmbl2  25453  voliunlem2  25468  ioombl1lem4  25478  ioorcl2  25489  uniioombllem1  25498  uniioombllem2a  25499  uniioombllem3  25502  dyaddisjlem  25512  dyadmaxlem  25514  opnmbllem  25518  volivth  25524  vitalilem4  25528  mbfmulc2lem  25564  mbfmax  25566  mbfposr  25569  ismbf3d  25571  mbfaddlem  25577  mbflimsup  25583  mbfi1fseqlem4  25635  itg2lcl  25644  xrge0f  25648  itg2itg1  25653  itg2const2  25658  itg2seq  25659  itg2uba  25660  itg2lea  25661  itg2mulclem  25663  itg2mulc  25664  itg2splitlem  25665  itg2split  25666  itg2monolem2  25668  itg2monolem3  25669  itg2mono  25670  itg2gt0  25677  itg2cnlem1  25678  itg2cnlem2  25679  itg2cn  25680  iblss  25722  itgle  25727  itgeqa  25731  itgioo  25733  ibladdlem  25737  iblabs  25746  iblabsr  25747  iblmulc2  25748  itgsplit  25753  itgspliticc  25754  itgsplitioo  25755  bddmulibl  25756  bddiblnc  25759  ditgcl  25775  ditgswap  25776  ditgsplitlem  25777  dvferm1lem  25904  dvferm2lem  25906  dvferm  25908  rollelem  25909  rolle  25910  cmvth  25911  cmvthOLD  25912  mvth  25913  dvlip  25914  dvlip2  25916  c1liplem1  25917  c1lip1  25918  dveq0  25921  dvgt0lem1  25923  dvivthlem1  25929  dvivth  25931  lhop1lem  25934  lhop1  25935  lhop2  25936  lhop  25937  dvcnvrelem1  25938  dvcnvre  25940  dvcvx  25941  dvfsumle  25942  dvfsumleOLD  25943  dvfsumge  25944  dvfsumabs  25945  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumlem3  25951  dvfsumlem4  25952  dvfsumrlimge0  25953  dvfsumrlim2  25955  ftc1lem1  25958  ftc1lem2  25959  ftc1a  25960  ftc1lem4  25962  ftc2  25967  ftc2ditglem  25968  itgparts  25970  itgsubstlem  25971  itgsubst  25972  itgpowd  25973  degltlem1  25993  deg1ge  26019  coe1mul3  26020  deg1sublt  26031  deg1mul2  26035  deg1tmle  26039  deg1tm  26040  idomrootle  26094  plypf1  26133  taylfvallem1  26280  tayl0  26285  pserulm  26347  psercnlem1  26351  pserdvlem1  26353  pserdvlem2  26354  abelthlem3  26359  abelth  26367  efcvx  26375  logno1  26561  logtayl  26585  xrlimcnp  26894  logfacbnd3  27150  log2sumbnd  27471  pntpbnd2  27514  pntibndlem3  27519  ttgcontlem1  28848  nmooge0  30729  nmoub3i  30735  isblo3i  30763  ubthlem1  30832  minvecolem4  30842  nmopge0  31873  nmfnge0  31889  nmophmi  31993  branmfn  32067  sgnval2  32691  xaddeq0  32709  xlt2addrd  32715  sgnmul  32793  sgnsub  32795  sgnmulsgn  32800  sgnmulsgp  32801  xmulcand  32874  xreceu  32875  xdivrec  32880  fsumrp0cl  32988  xrge0slmod  33298  ply1degltel  33539  ply1degleel  33540  ply1degltlss  33541  ply1degltdimlem  33597  ply1degltdim  33598  fldextrspundgdvdslem  33654  cos9thpiminplylem2  33752  cnre2csqlem  33879  tpr2rico  33881  xrge0iifcnv  33902  xrge0iifhom  33906  lmxrge0  33921  esumfsup  34039  esumpcvgval  34047  esumcvg  34055  dya2iocress  34244  dya2iocbrsiga  34245  dya2icobrsiga  34246  dya2icoseg  34247  dya2iocucvr  34254  sxbrsigalem2  34256  omssubaddlem  34269  omssubadd  34270  orvcgteel  34438  dstrvprob  34442  orvclteel  34443  signstcl  34535  signstf  34536  signstf0  34538  signstfvn  34539  signsvtn0  34540  signsvfn  34552  signsvfpn  34555  signsvfnn  34556  ftc2re  34568  cvmliftlem6  35265  cvmliftlem7  35266  cvmliftlem8  35267  cvmliftlem9  35268  cvmliftlem10  35269  cvmliftlem13  35271  ivthALT  36311  iooelexlt  37338  relowlssretop  37339  relowlpssretop  37340  sin2h  37592  cos2h  37593  tan2h  37594  poimirlem30  37632  poimir  37635  heicant  37637  opnmbllem0  37638  mblfinlem1  37639  mblfinlem2  37640  mblfinlem3  37641  mblfinlem4  37642  ismblfin  37643  itg2addnclem  37653  itg2addnclem2  37654  itg2gt0cn  37657  ibladdnclem  37658  iblabsnclem  37665  iblabsnc  37666  iblmulc2nc  37667  ftc1cnnclem  37673  ftc1anclem1  37675  ftc1anclem4  37678  ftc1anclem5  37679  ftc1anclem6  37680  ftc1anclem7  37681  ftc1anclem8  37682  ftc1anc  37683  ftc2nc  37684  areacirclem1  37690  areacirclem5  37694  areacirc  37695  isbnd3  37766  blbnd  37769  prdsbnd  37775  prdsbnd2  37777  cntotbnd  37778  dvrelog3  42041  0nonelalab  42043  dvrelogpow2b  42044  dvle2  42048  aks4d1p1p6  42049  aks4d1p1p5  42051  aks6d1c6lem3  42148  aks6d1c7lem2  42157  unitscyglem5  42175  idomodle  43167  imo72b2  44148  cvgdvgrat  44289  radcnvrat  44290  rfcnpre3  45014  rfcnpre4  45015  absfico  45199  nnxrd  45259  lefldiveq  45277  lttri5d  45284  supxrgere  45316  supxrgelem  45320  supxrge  45321  xralrple2  45337  infxr  45350  infleinflem1  45353  infleinflem2  45354  xralrple4  45356  xralrple3  45357  xrralrecnnle  45366  xrralrecnnge  45373  supxrunb3  45382  unb2ltle  45398  zxrd  45436  gtnelioc  45476  ltnelicc  45482  iooabslt  45484  gtnelicc  45485  eliooshift  45491  iocopn  45505  eliccelioc  45506  iooshift  45507  icoopn  45510  ge0lere  45517  iooiinicc  45527  sqrlearg  45538  iooiinioc  45541  uzinico  45544  preimaiocmnf  45545  uzubioo  45550  fsumge0cl  45558  limciccioolb  45606  lptioo1  45617  limcicciooub  45622  ltmod  45623  lptre2pt  45625  limsupre  45626  limcresiooub  45627  limcresioolb  45628  limcleqr  45629  limsupresico  45685  limsuppnfdlem  45686  limsupub  45689  limsupequzlem  45707  limsupre2lem  45709  limsupre3lem  45717  limsupvaluz2  45723  supcnvlimsup  45725  liminfresico  45756  limsup10exlem  45757  liminflelimsuplem  45760  limsupgtlem  45762  liminfval4  45774  liminfvaluz2  45780  limsupvaluz4  45785  liminflimsupclim  45792  xlimxrre  45816  xlimmnfvlem1  45817  xlimmnfv  45819  xlimpnfvlem1  45821  xlimpnfv  45823  sinaover2ne0  45853  ioccncflimc  45870  icccncfext  45872  icocncflimc  45874  cncfiooicclem1  45878  cncfiooicc  45879  cncfiooiccre  45880  cncfioobdlem  45881  dvbdfbdioolem1  45913  dvbdfbdioolem2  45914  dvbdfbdioo  45915  ioodvbdlimc1lem1  45916  ioodvbdlimc1lem2  45917  ioodvbdlimc1  45918  ioodvbdlimc2lem  45919  ioodvbdlimc2  45920  ditgeqiooicc  45945  iblsplit  45951  itgcoscmulx  45954  ibliooicc  45956  iblspltprt  45958  itgsincmulx  45959  itgsubsticc  45961  itgioocnicc  45962  iblcncfioo  45963  itgspltprt  45964  itgiccshift  45965  volioore  45975  voliooico  45977  voliooicof  45981  voliccico  45984  stoweidlem34  46019  stoweidlem52  46037  stirlinglem5  46063  dirkercncflem1  46088  dirkercncflem4  46091  fourierdlem4  46096  fourierdlem10  46102  fourierdlem19  46111  fourierdlem20  46112  fourierdlem24  46116  fourierdlem25  46117  fourierdlem26  46118  fourierdlem27  46119  fourierdlem28  46120  fourierdlem31  46123  fourierdlem32  46124  fourierdlem33  46125  fourierdlem35  46127  fourierdlem37  46129  fourierdlem40  46132  fourierdlem41  46133  fourierdlem43  46135  fourierdlem44  46136  fourierdlem46  46137  fourierdlem47  46138  fourierdlem48  46139  fourierdlem49  46140  fourierdlem50  46141  fourierdlem51  46142  fourierdlem52  46143  fourierdlem54  46145  fourierdlem57  46148  fourierdlem59  46150  fourierdlem60  46151  fourierdlem61  46152  fourierdlem62  46153  fourierdlem63  46154  fourierdlem64  46155  fourierdlem65  46156  fourierdlem68  46159  fourierdlem69  46160  fourierdlem70  46161  fourierdlem72  46163  fourierdlem73  46164  fourierdlem74  46165  fourierdlem75  46166  fourierdlem76  46167  fourierdlem78  46169  fourierdlem79  46170  fourierdlem81  46172  fourierdlem82  46173  fourierdlem84  46175  fourierdlem89  46180  fourierdlem90  46181  fourierdlem91  46182  fourierdlem92  46183  fourierdlem93  46184  fourierdlem94  46185  fourierdlem97  46188  fourierdlem100  46191  fourierdlem101  46192  fourierdlem102  46193  fourierdlem103  46194  fourierdlem104  46195  fourierdlem107  46198  fourierdlem109  46200  fourierdlem111  46202  fourierdlem112  46203  fourierdlem113  46204  fourierdlem114  46205  sqwvfoura  46213  fouriersw  46216  etransclem23  46242  etransclem46  46265  qndenserrnbllem  46279  rrxsnicc  46285  ioorrnopnlem  46289  ioorrnopnxrlem  46291  salgencntex  46328  sge0cl  46366  sge0fsum  46372  sge0iunmptlemre  46400  sge0isum  46412  sge0ad2en  46416  sge0xaddlem1  46418  sge0xaddlem2  46419  sge0reuz  46432  voliunsge0lem  46457  meassre  46462  omessre  46495  omeiunltfirp  46504  hoissre  46529  hoiprodcl  46532  ovnsubaddlem1  46555  hoiprodcl3  46565  hoidmvcl  46567  hsphoidmvle2  46570  hsphoidmvle  46571  sge0hsphoire  46574  hoidmv1lelem1  46576  hoidmv1lelem2  46577  hoidmv1lelem3  46578  hoidmv1le  46579  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem3  46582  hoidmvlelem4  46583  ovnhoilem1  46586  ovnhoilem2  46587  ovnhoi  46588  ovnlecvr2  46595  hspdifhsp  46601  hoidifhspdmvle  46605  hoiqssbllem1  46607  hoiqssbllem2  46608  hoiqssbllem3  46609  hspmbllem1  46611  hspmbllem2  46612  volicorege0  46622  ovolval5lem1  46637  ovolval5lem2  46638  iinhoiicclem  46658  iinhoiicc  46659  iunhoiioolem  46660  iunhoiioo  46661  vonioolem2  46666  vonicclem2  46669  vonsn  46676  pimltmnf2f  46682  pimconstlt0  46686  pimgtpnf2f  46690  salpreimagelt  46692  salpreimalegt  46694  preimageiingt  46705  preimaleiinlt  46706  pimrecltneg  46709  issmflem  46712  issmflelem  46729  issmfgtlem  46740  issmfgt  46741  smfaddlem1  46748  issmfgelem  46754  issmfge  46755  smfpimioompt  46771  smfresal  46773  smfrec  46774  smfmullem1  46776  smfmullem2  46777  smfmullem3  46778  smfmullem4  46779  smfpimbor1lem1  46783  smfsuplem1  46796  smflimsuplem4  46808  smfliminflem  46815  smfdmmblpimne  46822  smfpimne  46824  smfpimne2  46825  fsupdm  46827  finfdm  46831  smfinfdmmbllem  46833  bgoldbtbnd  47797  eenglngeehlnmlem2  48727