Theorem rexr 9429

Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
rexr	|- ( A e. RR -> A e. RR* )

Proof of Theorem rexr

Step	Hyp	Ref	Expression
1		ressxr 9427	. 2 |- RR C_ RR*
2	1	sseli 3352	1 |- ( A e. RR -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1756   RRcr 9281   RR*cxr 9417

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 2423

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 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-un 3333  df-in 3335  df-ss 3342  df-xr 9422

This theorem is referenced by:  rexri  9436  lenlt  9453  ltpnf  11102  mnflt  11104  xrltnsym  11114  xrlttr  11117  xrre  11141  xrre3  11143  max1  11157  max2  11159  min1  11160  min2  11161  maxle  11162  lemin  11163  maxlt  11164  ltmin  11165  max0sub  11166  qbtwnxr  11170  xralrple  11175  alrple  11176  xltnegi  11186  rexadd  11202  xaddnemnf  11204  xaddnepnf  11205  xaddcom  11208  xnegdi  11211  xpncan  11214  xnpcan  11215  xleadd1a  11216  xleadd1  11218  xltadd1  11219  xltadd2  11220  xsubge0  11224  rexmul  11234  xadddilem  11257  xadddir  11259  xrsupsslem  11269  xrinfmsslem  11270  xrub  11274  supxrun  11278  supxrunb1  11282  supxrunb2  11283  supxrbnd1  11284  supxrbnd2  11285  xrsup0  11286  supxrbnd  11291  elioo4g  11356  elioc2  11358  elico2  11359  elicc2  11360  iccss  11363  iooshf  11374  iooneg  11405  icoshft  11407  difreicc  11417  hashbnd  12109  sgn1  12581  elicc4abs  12807  limsupgord  12950  pcadd  13951  ramubcl  14079  lt6abl  16371  xrsmcmn  17839  xrs1mnd  17851  xrs10  17852  xrsdsreval  17858  psmetge0  19888  xmetge0  19919  imasdsf1olem  19948  bl2in  19975  blssps  19999  blss  20000  blcld  20080  icopnfcld  20347  iocmnfcld  20348  bl2ioo  20369  blssioo  20372  xrtgioo  20383  xrsblre  20388  iccntr  20398  icccmplem2  20400  icccmp  20402  reconnlem2  20404  xrge0tsms  20411  icoopnst  20511  iocopnst  20512  ovolfioo  20951  ovolicc2lem1  21000  ovolicc2lem5  21004  voliunlem3  21033  icombl1  21044  icombl  21045  iccvolcl  21048  ovolioo  21049  ioovolcl  21050  uniiccdif  21058  volsup2  21085  mbfimasn  21112  ismbf3d  21132  mbfsup  21142  itg2seq  21220  itg2monolem1  21228  itg2monolem2  21229  itg2monolem3  21230  itg2mono  21231  itg2i1fseqle  21232  itg2i1fseq3  21235  itg2addlem  21236  itg2gt0  21238  itg2cnlem2  21240  dvlip2  21467  ply1remlem  21634  abelthlem3  21898  abelth  21906  sincosq2sgn  21961  sincosq3sgn  21962  sinq12ge0  21970  sincos6thpi  21977  sineq0  21983  efif1olem1  21998  efif1olem2  21999  efif1o  22002  eff1o  22005  loglesqr  22196  basellem1  22418  pntlemo  22856  nmobndi  24175  nmopub2tALT  25313  nmfnleub2  25330  nmopcoadji  25505  rexdiv  26101  xrge0tsmsd  26253  pnfneige0  26381  lmxrge0  26382  hashf2  26533  sxbrsigalem0  26686  orvcgteel  26850  orvclteel  26855  sgnclre  26922  sgnneg  26923  signstfvneq0  26973  mblfinlem2  28429  itg2addnc  28446  itg2gt0cn  28447  iblabsnclem  28455  bddiblnc  28462  ftc1anclem1  28467  ftc1anclem6  28472  ftc1anclem8  28474  areacirclem5  28488  areacirc  28489  ivthALT  28530  blbnd  28686  icodiamlt  29161  iocmbl  29588