Theorem rexrd 9543

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

Syntax hints:   -> wi 4   e. wcel 1758   RRcr 9391   RR*cxr 9527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-un 3440  df-in 3442  df-ss 3449  df-xr 9532

This theorem is referenced by:  rpxr  11108  rpxrd  11138  max0sub  11276  qextltlem  11282  xralrple  11285  xnegcl  11293  xaddf  11304  xmulf  11345  xadddi  11368  supxrre  11400  infmxrre  11408  ixxub  11431  ixxlb  11432  ioo0  11435  ico0  11456  ioc0  11457  iooshf  11484  icoshftf1o  11524  supicc  11549  supiccub  11550  supicclub  11551  hashnnn0genn0  12230  elicc4abs  12924  caucvgrlem  13267  pcxcl  14044  pcdvdsb  14052  pcaddlem  14067  ramcl2lem  14187  ramlb  14197  0ram  14198  prdsxmetlem  20074  xblss2ps  20107  xblss2  20108  blss2ps  20109  blss2  20110  blhalf  20111  metusttoOLD  20263  metustto  20264  metustexhalfOLD  20269  metustexhalf  20270  nmoi  20438  nmoix  20439  nmoi2  20440  nmoleub  20441  qdensere  20480  cnblcld  20485  ioo2blex  20502  tgioo  20504  blcvx  20506  zcld  20521  recld2  20522  iccntr  20529  icccmplem1  20530  reconnlem1  20534  reconnlem2  20535  opnreen  20539  metnrmlem3  20568  cnheibor  20658  lebnumii  20669  nmoleub2lem  20800  lmnn  20905  iscau3  20920  minveclem4  21050  ivthlem1  21066  ivthlem2  21067  ivthlem3  21068  ivth2  21070  ivthle  21071  ivthle2  21072  ivthicc  21073  evthicc  21074  cniccbdd  21076  ovolgelb  21094  ovollb2lem  21102  ovolunlem1  21111  ovoliunlem1  21116  ovoliunlem2  21117  ovoliun  21119  ovolscalem1  21127  ovolicc1  21130  ovolicc2lem4  21134  ovolicc2lem5  21135  ovolicc2  21136  ovolicc  21137  nulmbl2  21150  voliunlem2  21164  ioombl1lem4  21174  ioorcl2  21184  uniioombllem1  21193  uniioombllem2a  21194  uniioombllem3  21197  dyaddisjlem  21207  dyadmaxlem  21209  opnmbllem  21213  volivth  21219  vitalilem4  21223  mbfmulc2lem  21257  mbfmax  21259  mbfposr  21262  ismbf3d  21264  mbfaddlem  21270  mbflimsup  21276  mbfi1fseqlem4  21328  itg2lcl  21337  xrge0f  21341  itg2itg1  21346  itg2const2  21351  itg2seq  21352  itg2uba  21353  itg2lea  21354  itg2mulclem  21356  itg2mulc  21357  itg2splitlem  21358  itg2split  21359  itg2monolem2  21361  itg2monolem3  21362  itg2mono  21363  itg2gt0  21370  itg2cnlem1  21371  itg2cnlem2  21372  itg2cn  21373  iblss  21414  itgle  21419  itgeqa  21423  itgioo  21425  ibladdlem  21429  iblabs  21438  iblabsr  21439  iblmulc2  21440  itgsplit  21445  itgspliticc  21446  itgsplitioo  21447  bddmulibl  21448  ditgcl  21465  ditgswap  21466  ditgsplitlem  21467  dvferm1lem  21588  dvferm2lem  21590  dvferm  21592  rollelem  21593  rolle  21594  cmvth  21595  mvth  21596  dvlip  21597  dvlip2  21599  c1liplem1  21600  c1lip1  21601  dveq0  21604  dvgt0lem1  21606  dvivthlem1  21612  dvivth  21614  lhop1lem  21617  lhop1  21618  lhop2  21619  lhop  21620  dvcnvrelem1  21621  dvcnvre  21623  dvcvx  21624  dvfsumle  21625  dvfsumge  21626  dvfsumabs  21627  dvfsumlem2  21631  dvfsumlem3  21632  dvfsumlem4  21633  dvfsumrlimge0  21634  dvfsumrlim2  21636  ftc1lem1  21639  ftc1lem2  21640  ftc1a  21641  ftc1lem4  21643  ftc2  21648  ftc2ditglem  21649  itgparts  21651  itgsubstlem  21652  itgsubst  21653  degltlem1  21675  deg1ge  21702  coe1mul3  21703  deg1sublt  21714  deg1mul2  21718  deg1tmle  21721  deg1tm  21722  plypf1  21812  taylfvallem1  21954  tayl0  21959  pserulm  22019  psercnlem1  22022  pserdvlem1  22024  pserdvlem2  22025  abelthlem3  22030  abelth  22038  efcvx  22046  logno1  22213  logtayl  22237  xrlimcnp  22494  logfacbnd3  22694  log2sumbnd  22925  pntpbnd2  22968  pntibndlem3  22973  ttgcontlem1  23282  nvlmle  24238  nmooge0  24318  nmoub3i  24324  isblo3i  24352  ubthlem1  24422  minvecolem4  24432  nmopge0  25466  nmfnge0  25482  nmophmi  25586  branmfn  25660  xaddeq0  26196  xlt2addrd  26201  xmulcand  26240  xreceu  26241  xdivrec  26246  fsumrp0cl  26302  xrge0slmod  26456  cnre2csqlem  26484  tpr2rico  26486  xrge0iifcnv  26507  xrge0iifhom  26511  lmxrge0  26526  esumfsup  26663  esumpcvgval  26671  esumcvg  26679  dya2iocress  26832  dya2iocbrsiga  26833  dya2icobrsiga  26834  dya2icoseg  26835  dya2iocucvr  26842  sxbrsigalem2  26844  orvcgteel  26993  dstrvprob  26997  orvclteel  26998  sgnmul  27068  sgnmulrp2  27069  sgnsub  27070  sgnmulsgn  27075  sgnmulsgp  27076  signstcl  27109  signstf  27110  signstf0  27112  signstfvn  27113  signsvtn0  27114  signstfvneq0  27116  signsvfn  27126  signsvfpn  27129  signsvfnn  27130  cvmliftlem6  27322  cvmliftlem7  27323  cvmliftlem8  27324  cvmliftlem9  27325  cvmliftlem10  27326  cvmliftlem13  27328  sin2h  28569  cos2h  28570  tan2h  28571  heicant  28573  opnmbllem0  28574  mblfinlem1  28575  mblfinlem2  28576  mblfinlem3  28577  mblfinlem4  28578  ismblfin  28579  dvtanlem  28588  itg2addnclem  28590  itg2addnclem2  28591  itg2gt0cn  28594  ibladdnclem  28595  iblabsnclem  28602  iblabsnc  28603  iblmulc2nc  28604  bddiblnc  28609  ftc1cnnclem  28612  ftc1anclem1  28614  ftc1anclem4  28617  ftc1anclem5  28618  ftc1anclem6  28619  ftc1anclem7  28620  ftc1anclem8  28621  ftc1anc  28622  ftc2nc  28623  areacirclem1  28631  areacirclem5  28635  areacirc  28636  ivthALT  28677  isbnd3  28830  blbnd  28833  prdsbnd  28839  prdsbnd2  28841  cntotbnd  28842  idomrootle  29707  idomodle  29708  itgpowd  29737  rfcnpre3  29902  rfcnpre4  29903  stoweidlem34  29976  stoweidlem52  29994  stirlinglem5  30020