Theorem rexr 10275

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

Assertion

Ref	Expression
rexr	⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Proof of Theorem rexr

Step	Hyp	Ref	Expression
1		ressxr 10273	. 2 ⊢ ℝ ⊆ ℝ*
2	1	sseli 3738	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2137  ℝcr 10125  ℝ^*cxr 10263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-v 3340  df-un 3718  df-in 3720  df-ss 3727  df-xr 10268

This theorem is referenced by:  rexri  10287  lenlt  10306  ltpnf  12145  mnflt  12148  xrltnsym  12161  xrlttr  12164  xrre  12191  xrre3  12193  max1  12207  max2  12209  min1  12211  min2  12212  maxle  12213  lemin  12214  maxlt  12215  ltmin  12216  max0sub  12218  qbtwnxr  12222  xralrple  12227  alrple  12228  xltnegi  12238  rexadd  12254  xaddnemnf  12258  xaddnepnf  12259  xaddcom  12262  xnegdi  12269  xpncan  12272  xnpcan  12273  xleadd1a  12274  xleadd1  12276  xltadd1  12277  xltadd2  12278  xsubge0  12282  rexmul  12292  xadddilem  12315  xadddir  12317  xrsupsslem  12328  xrinfmsslem  12329  xrub  12333  supxrun  12337  supxrunb1  12340  supxrunb2  12341  supxrbnd1  12342  supxrbnd2  12343  xrsup0  12344  supxrbnd  12349  infmremnf  12364  elioo4g  12425  elioc2  12427  elico2  12428  elicc2  12429  iccss  12432  iooshf  12443  iooneg  12483  icoshft  12485  difreicc  12495  hashbnd  13315  elicc4abs  14256  icodiamlt  14371  limsupgord  14400  pcadd  15793  ramubcl  15922  lt6abl  18494  xrsmcmn  19969  xrs1mnd  19984  xrs10  19985  xrsdsreval  19991  psmetge0  22316  xmetge0  22348  imasdsf1olem  22377  bl2in  22404  blssps  22428  blss  22429  blcld  22509  icopnfcld  22770  iocmnfcld  22771  bl2ioo  22794  blssioo  22797  xrtgioo  22808  xrsblre  22813  iccntr  22823  icccmplem2  22825  icccmp  22827  reconnlem2  22829  xrge0tsms  22836  icoopnst  22937  iocopnst  22938  ovolfioo  23434  ovolicc2lem1  23483  ovolicc2lem5  23487  voliunlem3  23518  icombl1  23529  icombl  23530  iccvolcl  23533  ovolioo  23534  ioovolcl  23536  uniiccdif  23544  volsup2  23571  mbfimasn  23598  ismbf3d  23618  mbfsup  23628  itg2seq  23706  dvlip2  23955  ply1remlem  24119  abelthlem3  24384  abelth  24392  sincosq2sgn  24448  sincosq3sgn  24449  sinq12ge0  24457  sincos6thpi  24464  sineq0  24470  efif1olem1  24485  efif1olem2  24486  efif1o  24489  eff1o  24492  loglesqrt  24696  basellem1  25004  pntlemo  25493  nmobndi  27937  nmopub2tALT  29075  nmfnleub2  29092  nmopcoadji  29267  rexdiv  29941  xrge0tsmsd  30092  pnfneige0  30304  lmxrge0  30305  hashf2  30453  sxbrsigalem0  30640  omssubadd  30669  orvcgteel  30836  orvclteel  30841  sgnclre  30908  sgnneg  30909  signstfvneq0  30956  ivthALT  32634  icorempt2  33508  icoreunrn  33516  iooelexlt  33519  relowlssretop  33520  relowlpssretop  33521  poimir  33753  mblfinlem2  33758  iblabsnclem  33784  bddiblnc  33791  ftc1anclem1  33796  ftc1anclem6  33801  areacirclem5  33815  areacirc  33816  blbnd  33897  iocmbl  38298  supxrre3  40037  supxrgere  40045  infrpge  40063  infxrunb2  40080  infxrbnd2  40081  infleinflem2  40083  xrralrecnnle  40098  supxrunb3  40119  supminfxr2  40195  xrpnf  40212  ioomidp  40241  limsupre  40374  limsupub  40437  limsuppnflem  40443  limsupre3lem  40465  liminfgord  40487  liminflelimsuplem  40508  limsupgtlem  40510  xlimmnfvlem2  40560  xlimmnfv  40561  xlimpnfvlem2  40564  xlimpnfv  40565  icccncfext  40601  volioc  40689  volico  40701  fourierdlem113  40937  meaiuninclem  41198  meaiuninc3v  41202  icoresmbl  41261  ovolval5lem1  41370  mbfresmf  41452  cnfsmf  41453  incsmf  41455  smfconst  41462  decsmf  41479  smfres  41501  smfco  41513  issmfle2d  41519  bgoldbtbndlem3  42203