Theorem rexrd 11182

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 11176	. 2 ⊢ ℝ ⊆ ℝ*
2		rexrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1, 2	sselid 3931	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11025  ℝ^*cxr 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-xr 11170

This theorem is referenced by:  xnn0xr  12479  rpxr  12915  rpxrd  12950  max0sub  13111  qextltlem  13117  xralrple  13120  xnegcl  13128  xaddf  13139  xnn0lem1lt  13159  xnn0lenn0nn0  13160  xmulf  13187  xadddi  13210  xrub  13227  supxrre  13242  infxrre  13252  ixxub  13282  ixxlb  13283  ioo0  13286  ico0  13307  ioc0  13308  iooshf  13342  icoshftf1o  13390  supicc  13417  supiccub  13418  supicclub  13419  xnn0xrge0  13422  ssfzunsn  13486  addmodid  13842  hashnnn0genn0  14266  hashunsnggt  14317  elicc4abs  15243  caucvgrlem  15596  fprodge1  15918  pcxcl  16789  pcdvdsb  16797  pcaddlem  16816  ramcl2lem  16937  ramlb  16947  0ram  16948  setsstruct  17103  prdsxmetlem  24312  xblss2ps  24345  xblss2  24346  blss2ps  24347  blss2  24348  blhalf  24349  metustto  24497  metustexhalf  24500  nmoi  24672  nmoix  24673  nmoi2  24674  nmoleub  24675  qdensere  24713  cnblcld  24718  ioo2blex  24738  tgioo  24740  blcvx  24742  zcld  24758  recld2  24759  iccntr  24766  icccmplem1  24767  reconnlem1  24771  reconnlem2  24772  opnreen  24776  metnrmlem3  24806  icoopnst  24892  iocopnst  24893  cnheibor  24910  lebnumii  24921  nmoleub2lem  25070  lmnn  25219  iscau3  25234  minveclem4  25388  ivthlem1  25408  ivthlem2  25409  ivthlem3  25410  ivth2  25412  ivthle  25413  ivthle2  25414  ivthicc  25415  evthicc  25416  cniccbdd  25418  ovolgelb  25437  ovollb2lem  25445  ovolunlem1  25454  ovoliunlem1  25459  ovoliunlem2  25460  ovoliun  25462  ovolscalem1  25470  ovolicc1  25473  ovolicc2lem4  25477  ovolicc2lem5  25478  ovolicc2  25479  ovolicc  25480  nulmbl2  25493  voliunlem2  25508  ioombl1lem4  25518  ioorcl2  25529  uniioombllem1  25538  uniioombllem2a  25539  uniioombllem3  25542  dyaddisjlem  25552  dyadmaxlem  25554  opnmbllem  25558  volivth  25564  vitalilem4  25568  mbfmulc2lem  25604  mbfmax  25606  mbfposr  25609  ismbf3d  25611  mbfaddlem  25617  mbflimsup  25623  mbfi1fseqlem4  25675  itg2lcl  25684  xrge0f  25688  itg2itg1  25693  itg2const2  25698  itg2seq  25699  itg2uba  25700  itg2lea  25701  itg2mulclem  25703  itg2mulc  25704  itg2splitlem  25705  itg2split  25706  itg2monolem2  25708  itg2monolem3  25709  itg2mono  25710  itg2gt0  25717  itg2cnlem1  25718  itg2cnlem2  25719  itg2cn  25720  iblss  25762  itgle  25767  itgeqa  25771  itgioo  25773  ibladdlem  25777  iblabs  25786  iblabsr  25787  iblmulc2  25788  itgsplit  25793  itgspliticc  25794  itgsplitioo  25795  bddmulibl  25796  bddiblnc  25799  ditgcl  25815  ditgswap  25816  ditgsplitlem  25817  dvferm1lem  25944  dvferm2lem  25946  dvferm  25948  rollelem  25949  rolle  25950  cmvth  25951  cmvthOLD  25952  mvth  25953  dvlip  25954  dvlip2  25956  c1liplem1  25957  c1lip1  25958  dveq0  25961  dvgt0lem1  25963  dvivthlem1  25969  dvivth  25971  lhop1lem  25974  lhop1  25975  lhop2  25976  lhop  25977  dvcnvrelem1  25978  dvcnvre  25980  dvcvx  25981  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem3  25991  dvfsumlem4  25992  dvfsumrlimge0  25993  dvfsumrlim2  25995  ftc1lem1  25998  ftc1lem2  25999  ftc1a  26000  ftc1lem4  26002  ftc2  26007  ftc2ditglem  26008  itgparts  26010  itgsubstlem  26011  itgsubst  26012  itgpowd  26013  degltlem1  26033  deg1ge  26059  coe1mul3  26060  deg1sublt  26071  deg1mul2  26075  deg1tmle  26079  deg1tm  26080  idomrootle  26134  plypf1  26173  taylfvallem1  26320  tayl0  26325  pserulm  26387  psercnlem1  26391  pserdvlem1  26393  pserdvlem2  26394  abelthlem3  26399  abelth  26407  efcvx  26415  logno1  26601  logtayl  26625  xrlimcnp  26934  logfacbnd3  27190  log2sumbnd  27511  pntpbnd2  27554  pntibndlem3  27559  ttgcontlem1  28957  nmooge0  30842  nmoub3i  30848  isblo3i  30876  ubthlem1  30945  minvecolem4  30955  nmopge0  31986  nmfnge0  32002  nmophmi  32106  branmfn  32180  sgnval2  32814  nn0mnfxrd  32831  xaddeq0  32833  xlt2addrd  32839  sgnmul  32916  sgnsub  32918  sgnmulsgn  32923  sgnmulsgp  32924  xmulcand  33002  xreceu  33003  xdivrec  33008  fsumrp0cl  33103  xrge0slmod  33429  ply1degltel  33675  ply1degleel  33676  ply1degltlss  33677  ply1degltdimlem  33779  ply1degltdim  33780  fldextrspundgdvdslem  33837  extdgfialglem1  33849  cos9thpiminplylem2  33940  cnre2csqlem  34067  tpr2rico  34069  xrge0iifcnv  34090  xrge0iifhom  34094  lmxrge0  34109  esumfsup  34227  esumpcvgval  34235  esumcvg  34243  dya2iocress  34431  dya2iocbrsiga  34432  dya2icobrsiga  34433  dya2icoseg  34434  dya2iocucvr  34441  sxbrsigalem2  34443  omssubaddlem  34456  omssubadd  34457  orvcgteel  34625  dstrvprob  34629  orvclteel  34630  signstcl  34722  signstf  34723  signstf0  34725  signstfvn  34726  signsvtn0  34727  signsvfn  34739  signsvfpn  34742  signsvfnn  34743  ftc2re  34755  cvmliftlem6  35484  cvmliftlem7  35485  cvmliftlem8  35486  cvmliftlem9  35487  cvmliftlem10  35488  cvmliftlem13  35490  ivthALT  36529  iooelexlt  37567  relowlssretop  37568  relowlpssretop  37569  sin2h  37811  cos2h  37812  tan2h  37813  poimirlem30  37851  poimir  37854  heicant  37856  opnmbllem0  37857  mblfinlem1  37858  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  itg2addnclem  37872  itg2addnclem2  37873  itg2gt0cn  37876  ibladdnclem  37877  iblabsnclem  37884  iblabsnc  37885  iblmulc2nc  37886  ftc1cnnclem  37892  ftc1anclem1  37894  ftc1anclem4  37897  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  ftc2nc  37903  areacirclem1  37909  areacirclem5  37913  areacirc  37914  isbnd3  37985  blbnd  37988  prdsbnd  37994  prdsbnd2  37996  cntotbnd  37997  dvrelog3  42319  0nonelalab  42321  dvrelogpow2b  42322  dvle2  42326  aks4d1p1p6  42327  aks4d1p1p5  42329  aks6d1c6lem3  42426  aks6d1c7lem2  42435  unitscyglem5  42453  idomodle  43433  imo72b2  44413  cvgdvgrat  44554  radcnvrat  44555  rfcnpre3  45278  rfcnpre4  45279  absfico  45462  nnxrd  45522  lefldiveq  45540  lttri5d  45547  supxrgere  45578  supxrgelem  45582  supxrge  45583  xralrple2  45599  infxr  45611  infleinflem1  45614  infleinflem2  45615  xralrple4  45617  xralrple3  45618  xrralrecnnle  45627  xrralrecnnge  45634  supxrunb3  45643  unb2ltle  45659  zxrd  45697  gtnelioc  45737  ltnelicc  45743  iooabslt  45745  gtnelicc  45746  eliooshift  45752  iocopn  45766  eliccelioc  45767  iooshift  45768  icoopn  45771  ge0lere  45778  iooiinicc  45788  sqrlearg  45799  iooiinioc  45802  uzinico  45805  preimaiocmnf  45806  uzubioo  45811  fsumge0cl  45819  limciccioolb  45867  lptioo1  45878  limcicciooub  45881  ltmod  45882  lptre2pt  45884  limsupre  45885  limcresiooub  45886  limcresioolb  45887  limcleqr  45888  limsupresico  45944  limsuppnfdlem  45945  limsupub  45948  limsupequzlem  45966  limsupre2lem  45968  limsupre3lem  45976  limsupvaluz2  45982  supcnvlimsup  45984  liminfresico  46015  limsup10exlem  46016  liminflelimsuplem  46019  limsupgtlem  46021  liminfval4  46033  liminfvaluz2  46039  limsupvaluz4  46044  liminflimsupclim  46051  xlimxrre  46075  xlimmnfvlem1  46076  xlimmnfv  46078  xlimpnfvlem1  46080  xlimpnfv  46082  sinaover2ne0  46112  ioccncflimc  46129  icccncfext  46131  icocncflimc  46133  cncfiooicclem1  46137  cncfiooicc  46138  cncfiooiccre  46139  cncfioobdlem  46140  dvbdfbdioolem1  46172  dvbdfbdioolem2  46173  dvbdfbdioo  46174  ioodvbdlimc1lem1  46175  ioodvbdlimc1lem2  46176  ioodvbdlimc1  46177  ioodvbdlimc2lem  46178  ioodvbdlimc2  46179  ditgeqiooicc  46204  iblsplit  46210  itgcoscmulx  46213  ibliooicc  46215  iblspltprt  46217  itgsincmulx  46218  itgsubsticc  46220  itgioocnicc  46221  iblcncfioo  46222  itgspltprt  46223  itgiccshift  46224  volioore  46234  voliooico  46236  voliooicof  46240  voliccico  46243  stoweidlem34  46278  stoweidlem52  46296  stirlinglem5  46322  dirkercncflem1  46347  dirkercncflem4  46350  fourierdlem4  46355  fourierdlem10  46361  fourierdlem19  46370  fourierdlem20  46371  fourierdlem24  46375  fourierdlem25  46376  fourierdlem26  46377  fourierdlem27  46378  fourierdlem28  46379  fourierdlem31  46382  fourierdlem32  46383  fourierdlem33  46384  fourierdlem35  46386  fourierdlem37  46388  fourierdlem40  46391  fourierdlem41  46392  fourierdlem43  46394  fourierdlem44  46395  fourierdlem46  46396  fourierdlem47  46397  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem51  46401  fourierdlem52  46402  fourierdlem54  46404  fourierdlem57  46407  fourierdlem59  46409  fourierdlem60  46410  fourierdlem61  46411  fourierdlem62  46412  fourierdlem63  46413  fourierdlem64  46414  fourierdlem65  46415  fourierdlem68  46418  fourierdlem69  46419  fourierdlem70  46420  fourierdlem72  46422  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem78  46428  fourierdlem79  46429  fourierdlem81  46431  fourierdlem82  46432  fourierdlem84  46434  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem92  46442  fourierdlem93  46443  fourierdlem94  46444  fourierdlem97  46447  fourierdlem100  46450  fourierdlem101  46451  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem107  46457  fourierdlem109  46459  fourierdlem111  46461  fourierdlem112  46462  fourierdlem113  46463  fourierdlem114  46464  sqwvfoura  46472  fouriersw  46475  etransclem23  46501  etransclem46  46524  qndenserrnbllem  46538  rrxsnicc  46544  ioorrnopnlem  46548  ioorrnopnxrlem  46550  salgencntex  46587  sge0cl  46625  sge0fsum  46631  sge0iunmptlemre  46659  sge0isum  46671  sge0ad2en  46675  sge0xaddlem1  46677  sge0xaddlem2  46678  sge0reuz  46691  voliunsge0lem  46716  meassre  46721  omessre  46754  omeiunltfirp  46763  hoissre  46788  hoiprodcl  46791  ovnsubaddlem1  46814  hoiprodcl3  46824  hoidmvcl  46826  hsphoidmvle2  46829  hsphoidmvle  46830  sge0hsphoire  46833  hoidmv1lelem1  46835  hoidmv1lelem2  46836  hoidmv1lelem3  46837  hoidmv1le  46838  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  ovnhoilem1  46845  ovnhoilem2  46846  ovnhoi  46847  ovnlecvr2  46854  hspdifhsp  46860  hoidifhspdmvle  46864  hoiqssbllem1  46866  hoiqssbllem2  46867  hoiqssbllem3  46868  hspmbllem1  46870  hspmbllem2  46871  volicorege0  46881  ovolval5lem1  46896  ovolval5lem2  46897  iinhoiicclem  46917  iinhoiicc  46918  iunhoiioolem  46919  iunhoiioo  46920  vonioolem2  46925  vonicclem2  46928  vonsn  46935  pimltmnf2f  46941  pimconstlt0  46945  pimgtpnf2f  46949  salpreimagelt  46951  salpreimalegt  46953  preimageiingt  46964  preimaleiinlt  46965  pimrecltneg  46968  issmflem  46971  issmflelem  46988  issmfgtlem  46999  issmfgt  47000  smfaddlem1  47007  issmfgelem  47013  issmfge  47014  smfpimioompt  47030  smfresal  47032  smfrec  47033  smfmullem1  47035  smfmullem2  47036  smfmullem3  47037  smfmullem4  47038  smfpimbor1lem1  47042  smfsuplem1  47055  smflimsuplem4  47067  smfliminflem  47074  smfdmmblpimne  47081  smfpimne  47083  smfpimne2  47084  fsupdm  47086  finfdm  47090  smfinfdmmbllem  47092  bgoldbtbnd  48055  eenglngeehlnmlem2  48984