Theorem rexr 10085

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 10083	. 2 ⊢ ℝ ⊆ ℝ*
2	1	sseli 3599	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 1990  ℝcr 9935  ℝ^*cxr 10073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-xr 10078

This theorem is referenced by:  rexri  10097  lenlt  10116  ltpnf  11954  mnflt  11957  xrltnsym  11970  xrlttr  11973  xrre  12000  xrre3  12002  max1  12016  max2  12018  min1  12020  min2  12021  maxle  12022  lemin  12023  maxlt  12024  ltmin  12025  max0sub  12027  qbtwnxr  12031  xralrple  12036  alrple  12037  xltnegi  12047  rexadd  12063  xaddnemnf  12067  xaddnepnf  12068  xaddcom  12071  xnegdi  12078  xpncan  12081  xnpcan  12082  xleadd1a  12083  xleadd1  12085  xltadd1  12086  xltadd2  12087  xsubge0  12091  rexmul  12101  xadddilem  12124  xadddir  12126  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  supxrun  12146  supxrunb1  12149  supxrunb2  12150  supxrbnd1  12151  supxrbnd2  12152  xrsup0  12153  supxrbnd  12158  infmremnf  12173  elioo4g  12234  elioc2  12236  elico2  12237  elicc2  12238  iccss  12241  iooshf  12252  iooneg  12292  icoshft  12294  difreicc  12304  hashbnd  13123  elicc4abs  14059  icodiamlt  14174  limsupgord  14203  pcadd  15593  ramubcl  15722  lt6abl  18296  xrsmcmn  19769  xrs1mnd  19784  xrs10  19785  xrsdsreval  19791  psmetge0  22117  xmetge0  22149  imasdsf1olem  22178  bl2in  22205  blssps  22229  blss  22230  blcld  22310  icopnfcld  22571  iocmnfcld  22572  bl2ioo  22595  blssioo  22598  xrtgioo  22609  xrsblre  22614  iccntr  22624  icccmplem2  22626  icccmp  22628  reconnlem2  22630  xrge0tsms  22637  icoopnst  22738  iocopnst  22739  ovolfioo  23236  ovolicc2lem1  23285  ovolicc2lem5  23289  voliunlem3  23320  icombl1  23331  icombl  23332  iccvolcl  23335  ovolioo  23336  ioovolcl  23338  uniiccdif  23346  volsup2  23373  mbfimasn  23401  ismbf3d  23421  mbfsup  23431  itg2seq  23509  dvlip2  23758  ply1remlem  23922  abelthlem3  24187  abelth  24195  sincosq2sgn  24251  sincosq3sgn  24252  sinq12ge0  24260  sincos6thpi  24267  sineq0  24273  efif1olem1  24288  efif1olem2  24289  efif1o  24292  eff1o  24295  loglesqrt  24499  basellem1  24807  pntlemo  25296  nmobndi  27630  nmopub2tALT  28768  nmfnleub2  28785  nmopcoadji  28960  rexdiv  29634  xrge0tsmsd  29785  pnfneige0  29997  lmxrge0  29998  hashf2  30146  sxbrsigalem0  30333  omssubadd  30362  orvcgteel  30529  orvclteel  30534  sgnclre  30601  sgnneg  30602  signstfvneq0  30649  ivthALT  32330  icorempt2  33199  icoreunrn  33207  iooelexlt  33210  relowlssretop  33211  relowlpssretop  33212  poimir  33442  mblfinlem2  33447  iblabsnclem  33473  bddiblnc  33480  ftc1anclem1  33485  ftc1anclem6  33490  areacirclem5  33504  areacirc  33505  blbnd  33586  iocmbl  37798  supxrre3  39541  supxrgere  39549  infrpge  39567  infxrunb2  39584  infxrbnd2  39585  infleinflem2  39587  xrralrecnnle  39602  supxrunb3  39623  supminfxr2  39699  ioomidp  39740  limsupre  39873  limsupub  39936  limsuppnflem  39942  limsupre3lem  39964  liminfgord  39986  liminflelimsuplem  40007  limsupgtlem  40009  xlimmnfvlem2  40059  xlimmnfv  40060  xlimpnfvlem2  40063  xlimpnfv  40064  icccncfext  40100  volioc  40188  volico  40200  fourierdlem113  40436  meaiuninclem  40697  icoresmbl  40757  ovolval5lem1  40866  mbfresmf  40948  cnfsmf  40949  incsmf  40951  smfconst  40958  decsmf  40975  smfres  40997  smfco  41009  issmfle2d  41015  bgoldbtbndlem3  41695