Theorem rexrd 9425

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 9419	. 2 |- RR C_ RR*
2		rexrd.1	. 2 |- ( ph -> A e. RR )
3	1, 2	sseldi 3349	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1756   RRcr 9273   RR*cxr 9409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328  df-in 3330  df-ss 3337  df-xr 9414

This theorem is referenced by:  rpxr  10990  rpxrd  11020  max0sub  11158  qextltlem  11164  xralrple  11167  xnegcl  11175  xaddf  11186  xmulf  11227  xadddi  11250  supxrre  11282  infmxrre  11290  ixxub  11313  ixxlb  11314  ioo0  11317  ico0  11338  ioc0  11339  iooshf  11366  icoshftf1o  11400  supicc  11425  supiccub  11426  supicclub  11427  hashnnn0genn0  12106  elicc4abs  12799  caucvgrlem  13142  pcxcl  13919  pcdvdsb  13927  pcaddlem  13942  ramcl2lem  14062  ramlb  14072  0ram  14073  prdsxmetlem  19923  xblss2ps  19956  xblss2  19957  blss2ps  19958  blss2  19959  blhalf  19960  metusttoOLD  20112  metustto  20113  metustexhalfOLD  20118  metustexhalf  20119  nmoi  20287  nmoix  20288  nmoi2  20289  nmoleub  20290  qdensere  20329  cnblcld  20334  ioo2blex  20351  tgioo  20353  blcvx  20355  zcld  20370  recld2  20371  iccntr  20378  icccmplem1  20379  reconnlem1  20383  reconnlem2  20384  opnreen  20388  metnrmlem3  20417  cnheibor  20507  lebnumii  20518  nmoleub2lem  20649  lmnn  20754  iscau3  20769  minveclem4  20899  ivthlem1  20915  ivthlem2  20916  ivthlem3  20917  ivth2  20919  ivthle  20920  ivthle2  20921  ivthicc  20922  evthicc  20923  cniccbdd  20925  ovolgelb  20943  ovollb2lem  20951  ovolunlem1  20960  ovoliunlem1  20965  ovoliunlem2  20966  ovoliun  20968  ovolscalem1  20976  ovolicc1  20979  ovolicc2lem4  20983  ovolicc2lem5  20984  ovolicc2  20985  ovolicc  20986  nulmbl2  20998  voliunlem2  21012  ioombl1lem4  21022  ioorcl2  21032  uniioombllem1  21041  uniioombllem2a  21042  uniioombllem3  21045  dyaddisjlem  21055  dyadmaxlem  21057  opnmbllem  21061  volivth  21067  vitalilem4  21071  mbfmulc2lem  21105  mbfmax  21107  mbfposr  21110  ismbf3d  21112  mbfaddlem  21118  mbflimsup  21124  mbfi1fseqlem4  21176  itg2lcl  21185  xrge0f  21189  itg2itg1  21194  itg2const2  21199  itg2seq  21200  itg2uba  21201  itg2lea  21202  itg2mulclem  21204  itg2mulc  21205  itg2splitlem  21206  itg2split  21207  itg2monolem2  21209  itg2monolem3  21210  itg2mono  21211  itg2gt0  21218  itg2cnlem1  21219  itg2cnlem2  21220  itg2cn  21221  iblss  21262  itgle  21267  itgeqa  21271  itgioo  21273  ibladdlem  21277  iblabs  21286  iblabsr  21287  iblmulc2  21288  itgsplit  21293  itgspliticc  21294  itgsplitioo  21295  bddmulibl  21296  ditgcl  21313  ditgswap  21314  ditgsplitlem  21315  dvferm1lem  21436  dvferm2lem  21438  dvferm  21440  rollelem  21441  rolle  21442  cmvth  21443  mvth  21444  dvlip  21445  dvlip2  21447  c1liplem1  21448  c1lip1  21449  dveq0  21452  dvgt0lem1  21454  dvivthlem1  21460  dvivth  21462  lhop1lem  21465  lhop1  21466  lhop2  21467  lhop  21468  dvcnvrelem1  21469  dvcnvre  21471  dvcvx  21472  dvfsumle  21473  dvfsumge  21474  dvfsumabs  21475  dvfsumlem2  21479  dvfsumlem3  21480  dvfsumlem4  21481  dvfsumrlimge0  21482  dvfsumrlim2  21484  ftc1lem1  21487  ftc1lem2  21488  ftc1a  21489  ftc1lem4  21491  ftc2  21496  ftc2ditglem  21497  itgparts  21499  itgsubstlem  21500  itgsubst  21501  degltlem1  21523  deg1ge  21550  coe1mul3  21551  deg1sublt  21562  deg1mul2  21566  deg1tmle  21569  deg1tm  21570  plypf1  21660  taylfvallem1  21802  tayl0  21807  pserulm  21867  psercnlem1  21870  pserdvlem1  21872  pserdvlem2  21873  abelthlem3  21878  abelth  21886  efcvx  21894  logno1  22061  logtayl  22085  xrlimcnp  22342  logfacbnd3  22542  log2sumbnd  22773  pntpbnd2  22816  pntibndlem3  22821  ttgcontlem1  23099  nvlmle  24055  nmooge0  24135  nmoub3i  24141  isblo3i  24169  ubthlem1  24239  minvecolem4  24249  nmopge0  25283  nmfnge0  25299  nmophmi  25403  branmfn  25477  xaddeq0  26014  xlt2addrd  26019  xmulcand  26064  xreceu  26065  xdivrec  26070  fsumrp0cl  26126  xrge0slmod  26281  cnre2csqlem  26309  tpr2rico  26311  xrge0iifcnv  26332  xrge0iifhom  26336  lmxrge0  26351  esumfsup  26488  esumpcvgval  26496  esumcvg  26504  dya2iocress  26658  dya2iocbrsiga  26659  dya2icobrsiga  26660  dya2icoseg  26661  dya2iocucvr  26668  sxbrsigalem2  26670  orvcgteel  26819  dstrvprob  26823  orvclteel  26824  sgnmul  26894  sgnmulrp2  26895  sgnsub  26896  sgnmulsgn  26901  sgnmulsgp  26902  signstcl  26935  signstf  26936  signstf0  26938  signstfvn  26939  signsvtn0  26940  signstfvneq0  26942  signsvfn  26952  signsvfpn  26955  signsvfnn  26956  cvmliftlem6  27148  cvmliftlem7  27149  cvmliftlem8  27150  cvmliftlem9  27151  cvmliftlem10  27152  cvmliftlem13  27154  sin2h  28393  cos2h  28394  tan2h  28395  heicant  28397  opnmbllem0  28398  mblfinlem1  28399  mblfinlem2  28400  mblfinlem3  28401  mblfinlem4  28402  ismblfin  28403  dvtanlem  28412  itg2addnclem  28414  itg2addnclem2  28415  itg2gt0cn  28418  ibladdnclem  28419  iblabsnclem  28426  iblabsnc  28427  iblmulc2nc  28428  bddiblnc  28433  ftc1cnnclem  28436  ftc1anclem1  28438  ftc1anclem4  28441  ftc1anclem5  28442  ftc1anclem6  28443  ftc1anclem7  28444  ftc1anclem8  28445  ftc1anc  28446  ftc2nc  28447  areacirclem1  28455  areacirclem5  28459  areacirc  28460  ivthALT  28501  isbnd3  28654  blbnd  28657  prdsbnd  28663  prdsbnd2  28665  cntotbnd  28666  idomrootle  29531  idomodle  29532  itgpowd  29561  rfcnpre3  29726  rfcnpre4  29727  stoweidlem34  29800  stoweidlem52  29818  stirlinglem5  29844