Theorem rexr 9704

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

Syntax hints:   -> wi 4   e. wcel 1904   RRcr 9556   RR*cxr 9692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395  df-in 3397  df-ss 3404  df-xr 9697

This theorem is referenced by:  rexri  9711  lenlt  9730  ltpnf  11445  mnflt  11448  xrltnsym  11459  xrlttr  11462  xrre  11487  xrre3  11489  max1  11503  max2  11505  min1  11506  min2  11507  maxle  11508  lemin  11509  maxlt  11510  ltmin  11511  max0sub  11512  qbtwnxr  11516  xralrple  11521  alrple  11522  xltnegi  11532  rexadd  11548  xaddnemnf  11551  xaddnepnf  11552  xaddcom  11555  xnegdi  11559  xpncan  11562  xnpcan  11563  xleadd1a  11564  xleadd1  11566  xltadd1  11567  xltadd2  11568  xsubge0  11572  rexmul  11582  xadddilem  11605  xadddir  11607  xrsupsslem  11617  xrinfmsslem  11618  xrub  11622  supxrun  11626  supxrunb1  11630  supxrunb2  11631  supxrbnd1  11632  supxrbnd2  11633  xrsup0  11634  supxrbnd  11639  infmremnf  11658  elioo4g  11720  elioc2  11722  elico2  11723  elicc2  11724  iccss  11727  iooshf  11738  iooneg  11778  icoshft  11780  difreicc  11790  hashbnd  12559  elicc4abs  13459  icodiamlt  13574  limsupgord  13605  pcadd  14913  ramubcl  15055  lt6abl  17607  xrsmcmn  19068  xrs1mnd  19083  xrs10  19084  xrsdsreval  19090  psmetge0  21406  xmetge0  21437  imasdsf1olem  21466  bl2in  21493  blssps  21517  blss  21518  blcld  21598  icopnfcld  21866  iocmnfcld  21867  bl2ioo  21888  blssioo  21891  xrtgioo  21902  xrsblre  21907  iccntr  21917  icccmplem2  21919  icccmp  21921  reconnlem2  21923  xrge0tsms  21930  icoopnst  22045  iocopnst  22046  ovolfioo  22498  ovolicc2lem1  22548  ovolicc2lem5  22553  voliunlem3  22584  icombl1  22595  icombl  22596  iccvolcl  22599  ovolioo  22600  ioovolcl  22601  uniiccdif  22614  volsup2  22642  mbfimasn  22669  ismbf3d  22689  mbfsup  22699  itg2seq  22779  dvlip2  23026  ply1remlem  23192  abelthlem3  23467  abelth  23475  sincosq2sgn  23533  sincosq3sgn  23534  sinq12ge0  23542  sincos6thpi  23549  sineq0  23555  efif1olem1  23570  efif1olem2  23571  efif1o  23574  eff1o  23577  loglesqrt  23777  basellem1  24086  pntlemo  24524  nmobndi  26497  nmopub2tALT  27643  nmfnleub2  27660  nmopcoadji  27835  rexdiv  28470  xrge0tsmsd  28622  pnfneige0  28831  lmxrge0  28832  hashf2  28979  sxbrsigalem0  29166  omssubadd  29201  omssubaddOLD  29205  orvcgteel  29373  orvclteel  29378  sgnclre  29483  sgnneg  29484  signstfvneq0  29533  ivthALT  31062  icorempt2  31824  icoreunrn  31832  iooelexlt  31835  relowlssretop  31836  relowlpssretop  31837  poimir  32037  mblfinlem2  32042  iblabsnclem  32069  bddiblnc  32076  ftc1anclem1  32081  ftc1anclem6  32086  areacirclem5  32100  areacirc  32101  blbnd  32183  iocmbl  36168  supxrre3  37635  supxrgere  37643  infrpge  37661  infxrunb2  37678  infxrbnd2  37679  infleinflem2  37681  ioomidp  37711  limsupre  37818  limsupreOLD  37819  icccncfext  37862  volioc  37946  volico  37958  fourierdlem113  38195  icoresmbl  38483  ovolval5lem1  38592  bgoldbtbndlem3  39047