Theorem rexri 9695

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

Syntax hints:   e. wcel 1869   RRcr 9540   RR*cxr 9676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-un 3442  df-in 3444  df-ss 3451  df-xr 9681

This theorem is referenced by:  xmulid1  11567  xmulid2  11568  xmulm1  11569  x2times  11587  xov1plusxeqvd  11780  ico01fl0  12054  hashge1  12569  hashgt12el  12594  hashgt12el2  12595  hashge2el2difr  12636  sgn1  13149  fprodge1  14042  tanhbnd  14208  isnzr2hash  18481  0ringnnzr  18486  xrsnsgrp  18997  leordtval2  20220  nmoid  21755  metnrmlem1a  21867  metnrmlem1  21868  metnrmlem1aOLD  21882  metnrmlem1OLD  21883  icopnfcnv  21962  icopnfhmeo  21963  iccpnfcnv  21964  iccpnfhmeo  21965  oprpiece1res1  21971  oprpiece1res2  21972  pcoass  22047  vitalilem4  22561  itg2monolem1  22700  itg2monolem3  22702  abelthlem3  23380  abelth  23388  neghalfpirx  23413  sincosq1sgn  23445  sincosq2sgn  23446  sincosq4sgn  23448  coseq00topi  23449  coseq0negpitopi  23450  tanabsge  23453  sinq12gt0  23454  cosq14gt0  23457  cosordlem  23472  tanord1  23478  tanord  23479  tanregt0  23480  negpitopissre  23481  ellogrn  23501  logimclad  23514  argregt0  23551  argimgt0  23553  argimlt0  23554  dvloglem  23585  logf1o2  23587  dvlog2lem  23589  efopnlem2  23594  isosctrlem1  23739  asinneg  23804  asinsinlem  23809  acoscos  23811  reasinsin  23814  atanlogsublem  23833  atantan  23841  atanbndlem  23843  atanbnd  23844  atan1  23846  scvxcvx  23903  dchrvmasumlem2  24328  dchrvmasumiflem1  24331  pntibndlem1  24419  pntibndlem2  24421  pntibnd  24423  pntlemc  24425  pnt  24444  padicabvf  24461  padicabvcxp  24462  tgldimor  24538  umgrafi  25041  vdgfrgragt2  25747  nmopun  27659  nmoptrii  27739  nmopcoi  27740  pjnmopi  27793  xlt2addrd  28338  xdivrec  28397  xrsmulgzz  28441  xrnarchi  28502  unitssxrge0  28708  xrge0iifcnv  28741  xrge0iifiso  28743  xrge0iifhom  28745  hasheuni  28908  ddemeas  29061  prob01  29248  sgnsgn  29421  bj-pinftyccb  31621  bj-minftyccb  31625  bj-pinftynminfty  31627  sin2h  31855  cos2h  31856  tan2h  31857  broucube  31894  asindmre  31947  dvasin  31948  dvacos  31949  areacirclem1  31952  areaquad  36027  imo72b2  36483  cvgdvgrat  36526  isosctrlem1ALT  37198  sineq0ALT  37201  supxrgelem  37408  xrlexaddrp  37423  itgsin0pilem1  37652  fourierdlem24  37819  fourierdlem38  37834  fourierdlem43  37840  fourierdlem44  37841  fourierdlem46  37842  fourierdlem62  37858  fourierdlem74  37870  fourierdlem75  37871  fourierdlem85  37881  fourierdlem88  37884  fourierdlem93  37889  fourierdlem102  37898  fourierdlem103  37899  fourierdlem104  37900  fourierdlem111  37907  fourierdlem112  37908  fourierdlem114  37910  sqwvfoura  37918  sqwvfourb  37919  fourierswlem  37920  fouriersw  37921  fouriercn  37922  ovn0lem  38168  bgoldbtbndlem1  38618  bgoldbtbnd  38622  umgrfi  38850  pgrpgt2nabl  39457  expnegico01  39621  regt1loggt0  39653  rege1logbrege0  39675  rege1logbzge0  39676  dignnld  39720