Theorem rexr 11191

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℝ^*cxr 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-xr 11183

This theorem is referenced by:  rexri  11203  lenlt  11224  ltpnf  13071  mnflt  13074  xrltnsym  13088  xrlttr  13091  xrre  13121  xrre3  13123  max1  13137  max2  13139  min1  13141  min2  13142  maxle  13143  lemin  13144  maxlt  13145  ltmin  13146  max0sub  13148  qbtwnxr  13152  xralrple  13157  alrple  13158  xltnegi  13168  rexadd  13184  xaddnemnf  13188  xaddnepnf  13189  xaddcom  13192  xnegdi  13200  xpncan  13203  xnpcan  13204  xleadd1a  13205  xleadd1  13207  xltadd1  13208  xltadd2  13209  xsubge0  13213  rexmul  13223  xadddilem  13246  xadddir  13248  xrsupsslem  13259  xrinfmsslem  13260  xrub  13264  supxrun  13268  supxrunb1  13271  supxrunb2  13272  supxrbnd1  13273  supxrbnd2  13274  xrsup0  13275  supxrbnd  13280  infmremnf  13296  elioo4g  13359  elioc2  13362  elico2  13363  elicc2  13364  iccss  13367  iooshf  13379  iooneg  13424  icoshft  13426  difreicc  13437  hashbnd  14298  elicc4abs  15282  icodiamlt  15400  limsupgord  15434  pcadd  16860  ramubcl  16989  lt6abl  19870  xrsmcmn  21375  xrsdsreval  21392  xrs1mnd  21420  xrs10  21421  psmetge0  24277  xmetge0  24309  imasdsf1olem  24338  bl2in  24365  blssps  24389  blss  24390  blcld  24470  icopnfcld  24732  iocmnfcld  24733  bl2ioo  24757  blssioo  24760  xrtgioo  24772  xrsblre  24777  iccntr  24787  icccmplem2  24789  icccmp  24791  reconnlem2  24793  xrge0tsms  24800  icoopnst  24906  iocopnst  24907  ovolfioo  25434  ovolicc2lem1  25484  ovolicc2lem5  25488  voliunlem3  25519  icombl1  25530  icombl  25531  iccvolcl  25534  ovolioo  25535  ioovolcl  25537  uniiccdif  25545  volsup2  25572  mbfimasn  25599  ismbf3d  25621  mbfsup  25631  itg2seq  25709  bddiblnc  25809  dvlip2  25962  ply1remlem  26130  abelthlem3  26398  abelth  26406  sincosq2sgn  26463  sincosq3sgn  26464  sinq12ge0  26472  sincos6thpi  26480  sineq0  26488  efif1olem1  26506  efif1olem2  26507  efif1o  26510  eff1o  26513  loglesqrt  26725  basellem1  27044  pntlemo  27570  nmobndi  30846  nmopub2tALT  31980  nmfnleub2  31997  nmopcoadji  32172  sgnclre  32905  sgnneg  32906  rexdiv  32985  xrge0tsmsd  33134  pnfneige0  34095  lmxrge0  34096  hashf2  34228  sxbrsigalem0  34415  orvcgteel  34612  orvclteel  34617  signstfvn  34713  signstfvneq0  34716  signsvfn  34726  ivthALT  36517  icorempo  37667  icoreunrn  37675  iooelexlt  37678  relowlssretop  37679  relowlpssretop  37680  poimir  37974  mblfinlem2  37979  iblabsnclem  38004  ftc1anclem1  38014  ftc1anclem6  38019  areacirclem5  38033  areacirc  38034  blbnd  38108  iocmbl  43641  reabssgn  44063  supxrre3  45755  supxrgere  45763  infrpge  45781  infxrunb2  45797  infxrbnd2  45798  infleinflem2  45800  xrralrecnnle  45812  supxrunb3  45828  supminfxr2  45897  xrpnf  45913  ioomidp  45944  limsupre  46069  limsupub  46132  limsuppnflem  46138  limsupre3lem  46160  liminfgord  46182  liminflelimsuplem  46203  limsupgtlem  46205  limsupub2  46240  xlimpnfxnegmnf  46242  xlimmnfvlem2  46261  xlimmnfv  46262  xlimpnfvlem2  46265  xlimpnfv  46266  icccncfext  46315  volioc  46400  volico  46411  fourierdlem113  46647  meaiuninclem  46908  meaiuninc3v  46912  icoresmbl  46971  ovolval5lem1  47080  mbfresmf  47167  cnfsmf  47168  incsmf  47170  smfconst  47177  decsmf  47195  smfres  47218  smfco  47230  issmfle2d  47237  finfdm  47274  bgoldbtbndlem3  48283  rrxsphere  49224  i0oii  49395  io1ii  49396