Theorem rexri 9434

Description: A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)

Hypothesis

Ref	Expression
rexri.1	|- A e. RR

Assertion

Ref	Expression
rexri	|- A e. RR*

Proof of Theorem rexri

Step	Hyp	Ref	Expression
1		rexri.1	. 2 |- A e. RR
2		rexr 9427	. 2 |- ( A e. RR -> A e. RR* )
3	1, 2	ax-mp 5	1 |- A e. RR*

Syntax hints:   e. wcel 1756   RRcr 9279   RR*cxr 9415

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 2422

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 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-un 3331  df-in 3333  df-ss 3340  df-xr 9420

This theorem is referenced by:  xmulid1  11240  xmulid2  11241  xmulm1  11242  x2times  11260  xov1plusxeqvd  11429  hashge1  12150  hashgt12el  12171  hashgt12el2  12172  tanhbnd  13443  leordtval2  18814  nmoid  20319  metnrmlem1a  20432  metnrmlem1  20433  icopnfcnv  20512  icopnfhmeo  20513  iccpnfcnv  20514  iccpnfhmeo  20515  oprpiece1res1  20521  oprpiece1res2  20522  pcoass  20594  vitalilem4  21089  itg2monolem1  21226  itg2monolem3  21228  abelthlem3  21896  abelth  21904  neghalfpirx  21926  sincosq1sgn  21958  sincosq4sgn  21961  coseq00topi  21962  coseq0negpitopi  21963  tanabsge  21966  sinq12gt0  21967  cosq14gt0  21970  cosordlem  21985  tanord1  21991  tanord  21992  tanregt0  21993  negpitopissre  21994  ellogrn  22009  logimclad  22022  argregt0  22057  argimgt0  22059  argimlt0  22060  dvloglem  22091  logf1o2  22093  dvlog2lem  22095  efopnlem2  22100  isosctrlem1  22214  asinneg  22279  asinsinlem  22284  acoscos  22286  reasinsin  22289  atanlogsublem  22308  atantan  22316  atanbndlem  22318  atanbnd  22319  atan1  22321  scvxcvx  22377  dchrvmasumlem2  22745  dchrvmasumiflem1  22748  pntibndlem1  22836  pntibndlem2  22838  pntibnd  22840  pntlemc  22842  pnt  22861  padicabvf  22878  padicabvcxp  22879  tgldimor  22953  umgrafi  23254  nmopun  25416  nmoptrii  25496  nmopcoi  25497  pjnmopi  25550  xlt2addrd  26049  xdivrec  26100  xrsmulgzz  26137  xrnarchi  26199  unitssxrge0  26328  xrge0iifcnv  26361  xrge0iifiso  26363  xrge0iifhom  26365  hasheuni  26532  ddemeas  26650  prob01  26794  sgnsgn  26929  sin2h  28419  cos2h  28420  tan2h  28421  asindmre  28476  dvasin  28477  dvacos  28478  areacirclem1  28481  areaquad  29589  itgsin0pilem1  29787  vdgfrgragt2  30617  pgrpgt2nabel  30766  isnzr2hash  30771  0rngnnzr  30775  isosctrlem1ALT  31667  sineq0ALT  31670  bj-flbi3  32524  bj-pinftyccb  32541  bj-minftyccb  32545  bj-pinftynminfty  32547