Theorem rexr 10681

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℝcr 10530  ℝ^*cxr 10668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3941  df-in 3943  df-ss 3952  df-xr 10673

This theorem is referenced by:  rexri  10693  lenlt  10713  ltpnf  12509  mnflt  12512  xrltnsym  12524  xrlttr  12527  xrre  12556  xrre3  12558  max1  12572  max2  12574  min1  12576  min2  12577  maxle  12578  lemin  12579  maxlt  12580  ltmin  12581  max0sub  12583  qbtwnxr  12587  xralrple  12592  alrple  12593  xltnegi  12603  rexadd  12619  xaddnemnf  12623  xaddnepnf  12624  xaddcom  12627  xnegdi  12635  xpncan  12638  xnpcan  12639  xleadd1a  12640  xleadd1  12642  xltadd1  12643  xltadd2  12644  xsubge0  12648  rexmul  12658  xadddilem  12681  xadddir  12683  xrsupsslem  12694  xrinfmsslem  12695  xrub  12699  supxrun  12703  supxrunb1  12706  supxrunb2  12707  supxrbnd1  12708  supxrbnd2  12709  xrsup0  12710  supxrbnd  12715  infmremnf  12730  elioo4g  12791  elioc2  12793  elico2  12794  elicc2  12795  iccss  12798  iooshf  12809  iooneg  12851  icoshft  12853  difreicc  12864  hashbnd  13690  elicc4abs  14673  icodiamlt  14789  limsupgord  14823  pcadd  16219  ramubcl  16348  lt6abl  19009  xrsmcmn  20562  xrs1mnd  20577  xrs10  20578  xrsdsreval  20584  psmetge0  22916  xmetge0  22948  imasdsf1olem  22977  bl2in  23004  blssps  23028  blss  23029  blcld  23109  icopnfcld  23370  iocmnfcld  23371  bl2ioo  23394  blssioo  23397  xrtgioo  23408  xrsblre  23413  iccntr  23423  icccmplem2  23425  icccmp  23427  reconnlem2  23429  xrge0tsms  23436  icoopnst  23537  iocopnst  23538  ovolfioo  24062  ovolicc2lem1  24112  ovolicc2lem5  24116  voliunlem3  24147  icombl1  24158  icombl  24159  iccvolcl  24162  ovolioo  24163  ioovolcl  24165  uniiccdif  24173  volsup2  24200  mbfimasn  24227  ismbf3d  24249  mbfsup  24259  itg2seq  24337  dvlip2  24586  ply1remlem  24750  abelthlem3  25015  abelth  25023  sincosq2sgn  25079  sincosq3sgn  25080  sinq12ge0  25088  sincos6thpi  25095  sineq0  25103  efif1olem1  25120  efif1olem2  25121  efif1o  25124  eff1o  25127  loglesqrt  25333  basellem1  25652  pntlemo  26177  nmobndi  28546  nmopub2tALT  29680  nmfnleub2  29697  nmopcoadji  29872  rexdiv  30597  xrge0tsmsd  30687  pnfneige0  31189  lmxrge0  31190  hashf2  31338  sxbrsigalem0  31524  orvcgteel  31720  orvclteel  31725  sgnclre  31792  sgnneg  31793  signstfvn  31834  signstfvneq0  31837  signsvfn  31847  ivthALT  33678  icorempo  34626  icoreunrn  34634  iooelexlt  34637  relowlssretop  34638  relowlpssretop  34639  poimir  34919  mblfinlem2  34924  iblabsnclem  34949  bddiblnc  34956  ftc1anclem1  34961  ftc1anclem6  34966  areacirclem5  34980  areacirc  34981  blbnd  35059  iocmbl  39812  supxrre3  41585  supxrgere  41593  infrpge  41611  infxrunb2  41628  infxrbnd2  41629  infleinflem2  41631  xrralrecnnle  41645  supxrunb3  41664  supminfxr2  41737  xrpnf  41754  ioomidp  41782  limsupre  41914  limsupub  41977  limsuppnflem  41983  limsupre3lem  42005  liminfgord  42027  liminflelimsuplem  42048  limsupgtlem  42050  limsupub2  42085  xlimpnfxnegmnf  42087  xlimmnfvlem2  42106  xlimmnfv  42107  xlimpnfvlem2  42110  xlimpnfv  42111  icccncfext  42162  volioc  42249  volico  42261  fourierdlem113  42497  meaiuninclem  42755  meaiuninc3v  42759  icoresmbl  42818  ovolval5lem1  42927  mbfresmf  43009  cnfsmf  43010  incsmf  43012  smfconst  43019  decsmf  43036  smfres  43058  smfco  43070  issmfle2d  43076  bgoldbtbndlem3  43965  rrxsphere  44728