Theorem rexri 9635

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 9628	. 2 |- ( A e. RR -> A e. RR* )
3	1, 2	ax-mp 5	1 |- A e. RR*

Syntax hints:   e. wcel 1823   RRcr 9480   RR*cxr 9616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-in 3468  df-ss 3475  df-xr 9621

This theorem is referenced by:  xmulid1  11474  xmulid2  11475  xmulm1  11476  x2times  11494  xov1plusxeqvd  11669  ico01fl0  11935  hashge1  12440  hashgt12el  12465  hashgt12el2  12466  sgn1  13007  tanhbnd  13978  isnzr2hash  18107  0ringnnzr  18112  xrsnsgrp  18649  leordtval2  19880  nmoid  21415  metnrmlem1a  21528  metnrmlem1  21529  icopnfcnv  21608  icopnfhmeo  21609  iccpnfcnv  21610  iccpnfhmeo  21611  oprpiece1res1  21617  oprpiece1res2  21618  pcoass  21690  vitalilem4  22186  itg2monolem1  22323  itg2monolem3  22325  abelthlem3  22994  abelth  23002  neghalfpirx  23025  sincosq1sgn  23057  sincosq2sgn  23058  sincosq4sgn  23060  coseq00topi  23061  coseq0negpitopi  23062  tanabsge  23065  sinq12gt0  23066  cosq14gt0  23069  cosordlem  23084  tanord1  23090  tanord  23091  tanregt0  23092  negpitopissre  23093  ellogrn  23113  logimclad  23126  argregt0  23163  argimgt0  23165  argimlt0  23166  dvloglem  23197  logf1o2  23199  dvlog2lem  23201  efopnlem2  23206  isosctrlem1  23349  asinneg  23414  asinsinlem  23419  acoscos  23421  reasinsin  23424  atanlogsublem  23443  atantan  23451  atanbndlem  23453  atanbnd  23454  atan1  23456  scvxcvx  23513  dchrvmasumlem2  23881  dchrvmasumiflem1  23884  pntibndlem1  23972  pntibndlem2  23974  pntibnd  23976  pntlemc  23978  pnt  23997  padicabvf  24014  padicabvcxp  24015  tgldimor  24094  umgrafi  24524  vdgfrgragt2  25229  nmopun  27131  nmoptrii  27211  nmopcoi  27212  pjnmopi  27265  xlt2addrd  27809  xdivrec  27857  xrsmulgzz  27900  xrnarchi  27962  unitssxrge0  28117  xrge0iifcnv  28150  xrge0iifiso  28152  xrge0iifhom  28154  hasheuni  28314  ddemeas  28445  prob01  28616  sgnsgn  28751  sin2h  30285  cos2h  30286  tan2h  30287  asindmre  30342  dvasin  30343  dvacos  30344  areacirclem1  30347  areaquad  31425  cvgdvgrat  31435  fprodge1  31837  itgsin0pilem1  31987  fourierdlem24  32152  fourierdlem38  32166  fourierdlem43  32171  fourierdlem44  32172  fourierdlem46  32174  fourierdlem62  32190  fourierdlem74  32202  fourierdlem75  32203  fourierdlem85  32213  fourierdlem88  32216  fourierdlem93  32221  fourierdlem102  32230  fourierdlem103  32231  fourierdlem104  32232  fourierdlem111  32239  fourierdlem112  32240  fourierdlem114  32242  sqwvfoura  32250  sqwvfourb  32251  fourierswlem  32252  fouriersw  32253  fouriercn  32254  pgrpgt2nabl  33213  expnegico01  33377  regt1loggt0  33411  rege1logbrege0  33433  rege1logbzge0  33434  dignnld  33478  isosctrlem1ALT  34135  sineq0ALT  34138  bj-pinftyccb  35024  bj-minftyccb  35028  bj-pinftynminfty  35030  imo72b2  38445