Theorem rexri 9718

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

Syntax hints:   e. wcel 1897   RRcr 9563   RR*cxr 9699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-un 3420  df-in 3422  df-ss 3429  df-xr 9704

This theorem is referenced by:  xmulid1  11593  xmulid2  11594  xmulm1  11595  x2times  11613  xov1plusxeqvd  11806  ico01fl0  12084  hashge1  12599  hashgt12el  12627  hashgt12el2  12628  hashge2el2difr  12670  sgn1  13203  fprodge1  14097  tanhbnd  14263  isnzr2hash  18536  0ringnnzr  18541  xrsnsgrp  19052  leordtval2  20276  nmoid  21811  metnrmlem1a  21923  metnrmlem1  21924  metnrmlem1aOLD  21938  metnrmlem1OLD  21939  icopnfcnv  22018  icopnfhmeo  22019  iccpnfcnv  22020  iccpnfhmeo  22021  oprpiece1res1  22027  oprpiece1res2  22028  pcoass  22103  vitalilem4  22617  itg2monolem1  22756  itg2monolem3  22758  abelthlem3  23436  abelth  23444  neghalfpirx  23469  sincosq1sgn  23501  sincosq2sgn  23502  sincosq4sgn  23504  coseq00topi  23505  coseq0negpitopi  23506  tanabsge  23509  sinq12gt0  23510  cosq14gt0  23513  cosordlem  23528  tanord1  23534  tanord  23535  tanregt0  23536  negpitopissre  23537  ellogrn  23557  logimclad  23570  argregt0  23607  argimgt0  23609  argimlt0  23610  dvloglem  23641  logf1o2  23643  dvlog2lem  23645  efopnlem2  23650  isosctrlem1  23795  asinneg  23860  asinsinlem  23865  acoscos  23867  reasinsin  23870  atanlogsublem  23889  atantan  23897  atanbndlem  23899  atanbnd  23900  atan1  23902  scvxcvx  23959  dchrvmasumlem2  24384  dchrvmasumiflem1  24387  pntibndlem1  24475  pntibndlem2  24477  pntibnd  24479  pntlemc  24481  pnt  24500  padicabvf  24517  padicabvcxp  24518  tgldimor  24594  umgrafi  25097  vdgfrgragt2  25803  nmopun  27715  nmoptrii  27795  nmopcoi  27796  pjnmopi  27849  xlt2addrd  28386  xdivrec  28444  xrsmulgzz  28488  xrnarchi  28549  unitssxrge0  28754  xrge0iifcnv  28787  xrge0iifiso  28789  xrge0iifhom  28791  hasheuni  28954  ddemeas  29107  prob01  29294  sgnsgn  29467  bj-pinftyccb  31707  bj-minftyccb  31711  bj-pinftynminfty  31713  sin2h  31979  cos2h  31980  tan2h  31981  broucube  32018  asindmre  32071  dvasin  32072  dvacos  32073  areacirclem1  32076  areaquad  36145  imo72b2  36662  cvgdvgrat  36705  isosctrlem1ALT  37370  sineq0ALT  37373  supxrgelem  37597  xrlexaddrp  37612  itgsin0pilem1  37863  fourierdlem24  38030  fourierdlem38  38045  fourierdlem43  38051  fourierdlem44  38052  fourierdlem46  38053  fourierdlem62  38069  fourierdlem74  38081  fourierdlem75  38082  fourierdlem85  38092  fourierdlem88  38095  fourierdlem93  38100  fourierdlem102  38109  fourierdlem103  38110  fourierdlem104  38111  fourierdlem111  38118  fourierdlem112  38119  fourierdlem114  38121  sqwvfoura  38129  sqwvfourb  38130  fourierswlem  38131  fouriersw  38132  fouriercn  38133  salexct2  38235  salgencntex  38239  ovn0lem  38424  bgoldbtbndlem1  38937  bgoldbtbnd  38941  upgrfi  39229  upgrewlkle2  39672  umgrislfupgrlem  39717  upgr2pthnlp  39764  pgrpgt2nabl  40423  expnegico01  40587  regt1loggt0  40619  rege1logbrege0  40641  rege1logbzge0  40642  dignnld  40686