Theorem rexrd 9421

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

Hypothesis

Ref	Expression
rexrd.1	|- ( ph -> A e. RR )

Assertion

Ref	Expression
rexrd	|- ( ph -> A e. RR* )

Proof of Theorem rexrd

Step	Hyp	Ref	Expression
1		ressxr 9415	. 2 |- RR C_ RR*
2		rexrd.1	. 2 |- ( ph -> A e. RR )
3	1, 2	sseldi 3342	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1755   RRcr 9269   RR*cxr 9405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-in 3323  df-ss 3330  df-xr 9410

This theorem is referenced by:  rpxr  10986  rpxrd  11016  max0sub  11154  qextltlem  11160  xralrple  11163  xnegcl  11171  xaddf  11182  xmulf  11223  xadddi  11246  supxrre  11278  infmxrre  11286  ixxub  11309  ixxlb  11310  ioo0  11313  ico0  11334  ioc0  11335  iooshf  11362  icoshftf1o  11395  supicc  11420  supiccub  11421  supicclub  11422  hashnnn0genn0  12098  elicc4abs  12791  caucvgrlem  13134  pcxcl  13910  pcdvdsb  13918  pcaddlem  13933  ramcl2lem  14053  ramlb  14063  0ram  14064  prdsxmetlem  19785  xblss2ps  19818  xblss2  19819  blss2ps  19820  blss2  19821  blhalf  19822  metusttoOLD  19974  metustto  19975  metustexhalfOLD  19980  metustexhalf  19981  nmoi  20149  nmoix  20150  nmoi2  20151  nmoleub  20152  qdensere  20191  cnblcld  20196  ioo2blex  20213  tgioo  20215  blcvx  20217  zcld  20232  recld2  20233  iccntr  20240  icccmplem1  20241  reconnlem1  20245  reconnlem2  20246  opnreen  20250  metnrmlem3  20279  cnheibor  20369  lebnumii  20380  nmoleub2lem  20511  lmnn  20616  iscau3  20631  minveclem4  20761  ivthlem1  20777  ivthlem2  20778  ivthlem3  20779  ivth2  20781  ivthle  20782  ivthle2  20783  ivthicc  20784  evthicc  20785  cniccbdd  20787  ovolgelb  20805  ovollb2lem  20813  ovolunlem1  20822  ovoliunlem1  20827  ovoliunlem2  20828  ovoliun  20830  ovolscalem1  20838  ovolicc1  20841  ovolicc2lem4  20845  ovolicc2lem5  20846  ovolicc2  20847  ovolicc  20848  nulmbl2  20860  voliunlem2  20874  ioombl1lem4  20884  ioorcl2  20894  uniioombllem1  20903  uniioombllem2a  20904  uniioombllem3  20907  dyaddisjlem  20917  dyadmaxlem  20919  opnmbllem  20923  volivth  20929  vitalilem4  20933  mbfmulc2lem  20967  mbfmax  20969  mbfposr  20972  ismbf3d  20974  mbfaddlem  20980  mbflimsup  20986  mbfi1fseqlem4  21038  itg2lcl  21047  xrge0f  21051  itg2itg1  21056  itg2const2  21061  itg2seq  21062  itg2uba  21063  itg2lea  21064  itg2mulclem  21066  itg2mulc  21067  itg2splitlem  21068  itg2split  21069  itg2monolem2  21071  itg2monolem3  21072  itg2mono  21073  itg2gt0  21080  itg2cnlem1  21081  itg2cnlem2  21082  itg2cn  21083  iblss  21124  itgle  21129  itgeqa  21133  itgioo  21135  ibladdlem  21139  iblabs  21148  iblabsr  21149  iblmulc2  21150  itgsplit  21155  itgspliticc  21156  itgsplitioo  21157  bddmulibl  21158  ditgcl  21175  ditgswap  21176  ditgsplitlem  21177  dvferm1lem  21298  dvferm2lem  21300  dvferm  21302  rollelem  21303  rolle  21304  cmvth  21305  mvth  21306  dvlip  21307  dvlip2  21309  c1liplem1  21310  c1lip1  21311  dveq0  21314  dvgt0lem1  21316  dvivthlem1  21322  dvivth  21324  lhop1lem  21327  lhop1  21328  lhop2  21329  lhop  21330  dvcnvrelem1  21331  dvcnvre  21333  dvcvx  21334  dvfsumle  21335  dvfsumge  21336  dvfsumabs  21337  dvfsumlem2  21341  dvfsumlem3  21342  dvfsumlem4  21343  dvfsumrlimge0  21344  dvfsumrlim2  21346  ftc1lem1  21349  ftc1lem2  21350  ftc1a  21351  ftc1lem4  21353  ftc2  21358  ftc2ditglem  21359  itgparts  21361  itgsubstlem  21362  itgsubst  21363  degltlem1  21428  deg1ge  21455  coe1mul3  21456  deg1sublt  21467  deg1mul2  21471  deg1tmle  21474  deg1tm  21475  plypf1  21565  taylfvallem1  21707  tayl0  21712  pserulm  21772  psercnlem1  21775  pserdvlem1  21777  pserdvlem2  21778  abelthlem3  21783  abelth  21791  efcvx  21799  logno1  21966  logtayl  21990  xrlimcnp  22247  logfacbnd3  22447  log2sumbnd  22678  pntpbnd2  22721  pntibndlem3  22726  ttgcontlem1  22954  nvlmle  23910  nmooge0  23990  nmoub3i  23996  isblo3i  24024  ubthlem1  24094  minvecolem4  24104  nmopge0  25138  nmfnge0  25154  nmophmi  25258  branmfn  25332  xaddeq0  25871  xlt2addrd  25876  xmulcand  25919  xreceu  25920  xdivrec  25925  fsumrp0cl  25982  xrge0slmod  26166  cnre2csqlem  26194  tpr2rico  26196  xrge0iifcnv  26217  xrge0iifhom  26221  lmxrge0  26236  esumfsup  26373  esumpcvgval  26381  esumcvg  26389  dya2iocress  26543  dya2iocbrsiga  26544  dya2icobrsiga  26545  dya2icoseg  26546  dya2iocucvr  26553  sxbrsigalem2  26555  orvcgteel  26698  dstrvprob  26702  orvclteel  26703  sgnmul  26773  sgnmulrp2  26774  sgnsub  26775  sgnmulsgn  26780  sgnmulsgp  26781  signstcl  26814  signstf  26815  signstf0  26817  signstfvn  26818  signsvtn0  26819  signstfvneq0  26821  signsvfn  26831  signsvfpn  26834  signsvfnn  26835  cvmliftlem6  27027  cvmliftlem7  27028  cvmliftlem8  27029  cvmliftlem9  27030  cvmliftlem10  27031  cvmliftlem13  27033  sin2h  28266  cos2h  28267  tan2h  28268  heicant  28270  opnmbllem0  28271  mblfinlem1  28272  mblfinlem2  28273  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  dvtanlem  28285  itg2addnclem  28287  itg2addnclem2  28288  itg2gt0cn  28291  ibladdnclem  28292  iblabsnclem  28299  iblabsnc  28300  iblmulc2nc  28301  bddiblnc  28306  ftc1cnnclem  28309  ftc1anclem1  28311  ftc1anclem4  28314  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  ftc2nc  28320  areacirclem1  28328  areacirclem5  28332  areacirc  28333  ivthALT  28374  isbnd3  28527  blbnd  28530  prdsbnd  28536  prdsbnd2  28538  cntotbnd  28539  idomrootle  29405  idomodle  29406  itgpowd  29435  rfcnpre3  29600  rfcnpre4  29601  stoweidlem34  29675  stoweidlem52  29693  stirlinglem5  29719