Theorem rexr 9628

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

Syntax hints:   -> wi 4   e. wcel 1823   RRcr 9480   RR*cxr 9616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-in 3468  df-ss 3475  df-xr 9621

This theorem is referenced by:  rexri  9635  lenlt  9652  ltpnf  11334  mnflt  11336  xrltnsym  11346  xrlttr  11349  xrre  11373  xrre3  11375  max1  11389  max2  11391  min1  11392  min2  11393  maxle  11394  lemin  11395  maxlt  11396  ltmin  11397  max0sub  11398  qbtwnxr  11402  xralrple  11407  alrple  11408  xltnegi  11418  rexadd  11434  xaddnemnf  11436  xaddnepnf  11437  xaddcom  11440  xnegdi  11443  xpncan  11446  xnpcan  11447  xleadd1a  11448  xleadd1  11450  xltadd1  11451  xltadd2  11452  xsubge0  11456  rexmul  11466  xadddilem  11489  xadddir  11491  xrsupsslem  11501  xrinfmsslem  11502  xrub  11506  supxrun  11510  supxrunb1  11514  supxrunb2  11515  supxrbnd1  11516  supxrbnd2  11517  xrsup0  11518  supxrbnd  11523  elioo4g  11588  elioc2  11590  elico2  11591  elicc2  11592  iccss  11595  iooshf  11606  iooneg  11643  icoshft  11645  difreicc  11655  hashbnd  12393  elicc4abs  13234  limsupgord  13377  pcadd  14492  ramubcl  14620  lt6abl  17096  xrsmcmn  18636  xrs1mnd  18651  xrs10  18652  xrsdsreval  18658  psmetge0  20982  xmetge0  21013  imasdsf1olem  21042  bl2in  21069  blssps  21093  blss  21094  blcld  21174  icopnfcld  21441  iocmnfcld  21442  bl2ioo  21463  blssioo  21466  xrtgioo  21477  xrsblre  21482  iccntr  21492  icccmplem2  21494  icccmp  21496  reconnlem2  21498  xrge0tsms  21505  icoopnst  21605  iocopnst  21606  ovolfioo  22045  ovolicc2lem1  22094  ovolicc2lem5  22098  voliunlem3  22128  icombl1  22139  icombl  22140  iccvolcl  22143  ovolioo  22144  ioovolcl  22145  uniiccdif  22153  volsup2  22180  mbfimasn  22207  ismbf3d  22227  mbfsup  22237  itg2seq  22315  dvlip2  22562  ply1remlem  22729  abelthlem3  22994  abelth  23002  sincosq2sgn  23058  sincosq3sgn  23059  sinq12ge0  23067  sincos6thpi  23074  sineq0  23080  efif1olem1  23095  efif1olem2  23096  efif1o  23099  eff1o  23102  loglesqrt  23300  basellem1  23552  pntlemo  23990  nmobndi  25888  nmopub2tALT  27026  nmfnleub2  27043  nmopcoadji  27218  rexdiv  27856  xrge0tsmsd  28010  pnfneige0  28168  lmxrge0  28169  hashf2  28313  sxbrsigalem0  28479  omssubadd  28508  orvcgteel  28670  orvclteel  28675  sgnclre  28742  sgnneg  28743  signstfvneq0  28793  mblfinlem2  30292  iblabsnclem  30318  bddiblnc  30325  ftc1anclem1  30330  ftc1anclem6  30335  areacirclem5  30351  areacirc  30352  ivthALT  30393  blbnd  30523  icodiamlt  30995  iocmbl  31421  ioomidp  31793  limsupre  31886  icccncfext  31929  volioc  32010  fourierdlem113  32241