Theorem rexr 9425

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 9423	. 2 |- RR C_ RR*
2	1	sseli 3349	1 |- ( A e. RR -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1761   RRcr 9277   RR*cxr 9413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-un 3330  df-in 3332  df-ss 3339  df-xr 9418

This theorem is referenced by:  rexri  9432  lenlt  9449  ltpnf  11098  mnflt  11100  xrltnsym  11110  xrlttr  11113  xrre  11137  xrre3  11139  max1  11153  max2  11155  min1  11156  min2  11157  maxle  11158  lemin  11159  maxlt  11160  ltmin  11161  max0sub  11162  qbtwnxr  11166  xralrple  11171  alrple  11172  xltnegi  11182  rexadd  11198  xaddnemnf  11200  xaddnepnf  11201  xaddcom  11204  xnegdi  11207  xpncan  11210  xnpcan  11211  xleadd1a  11212  xleadd1  11214  xltadd1  11215  xltadd2  11216  xsubge0  11220  rexmul  11230  xadddilem  11253  xadddir  11255  xrsupsslem  11265  xrinfmsslem  11266  xrub  11270  supxrun  11274  supxrunb1  11278  supxrunb2  11279  supxrbnd1  11280  supxrbnd2  11281  xrsup0  11282  supxrbnd  11287  elioo4g  11352  elioc2  11354  elico2  11355  elicc2  11356  iccss  11359  iooshf  11370  iooneg  11401  icoshft  11403  difreicc  11413  hashbnd  12105  sgn1  12577  elicc4abs  12803  limsupgord  12946  pcadd  13947  ramubcl  14075  lt6abl  16364  xrsmcmn  17739  xrs1mnd  17751  xrs10  17752  xrsdsreval  17758  psmetge0  19788  xmetge0  19819  imasdsf1olem  19848  bl2in  19875  blssps  19899  blss  19900  blcld  19980  icopnfcld  20247  iocmnfcld  20248  bl2ioo  20269  blssioo  20272  xrtgioo  20283  xrsblre  20288  iccntr  20298  icccmplem2  20300  icccmp  20302  reconnlem2  20304  xrge0tsms  20311  icoopnst  20411  iocopnst  20412  ovolfioo  20851  ovolicc2lem1  20900  ovolicc2lem5  20904  voliunlem3  20933  icombl1  20944  icombl  20945  iccvolcl  20948  ovolioo  20949  ioovolcl  20950  uniiccdif  20958  volsup2  20985  mbfimasn  21012  ismbf3d  21032  mbfsup  21042  itg2seq  21120  itg2monolem1  21128  itg2monolem2  21129  itg2monolem3  21130  itg2mono  21131  itg2i1fseqle  21132  itg2i1fseq3  21135  itg2addlem  21136  itg2gt0  21138  itg2cnlem2  21140  dvlip2  21367  ply1remlem  21577  abelthlem3  21841  abelth  21849  sincosq2sgn  21904  sincosq3sgn  21905  sinq12ge0  21913  sincos6thpi  21920  sineq0  21926  efif1olem1  21941  efif1olem2  21942  efif1o  21945  eff1o  21948  loglesqr  22139  basellem1  22361  pntlemo  22799  nmobndi  24094  nmopub2tALT  25232  nmfnleub2  25249  nmopcoadji  25424  rexdiv  26018  xrge0tsmsd  26172  pnfneige0  26301  lmxrge0  26302  hashf2  26453  sxbrsigalem0  26606  orvcgteel  26764  orvclteel  26769  sgnclre  26836  sgnneg  26837  signstfvneq0  26887  mblfinlem2  28338  itg2addnc  28355  itg2gt0cn  28356  iblabsnclem  28364  bddiblnc  28371  ftc1anclem1  28376  ftc1anclem6  28381  ftc1anclem8  28383  areacirclem5  28397  areacirc  28398  ivthALT  28439  blbnd  28595  icodiamlt  29070  iocmbl  29497