Theorem rexri 11042

Description: A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)

Hypothesis

Ref	Expression
rexri.1	⊢ 𝐴 ∈ ℝ

Assertion

Ref	Expression
rexri	⊢ 𝐴 ∈ ℝ*

Proof of Theorem rexri

Step	Hyp	Ref	Expression
1		rexri.1	. 2 ⊢ 𝐴 ∈ ℝ
2		rexr 11030	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ ℝ*

Syntax hints:   ∈ wcel 2107  ℝcr 10879  ℝ^*cxr 11017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-in 3895  df-ss 3905  df-xr 11022

This theorem is referenced by:  1xr  11043  xnn0n0n1ge2b  12876  hashgt23el  14148  hashge2el2difr  14204  tanhbnd  15879  halfleoddlt  16080  oprpiece1res1  24123  oprpiece1res2  24124  pcoass  24196  vitalilem4  24784  neghalfpirx  25632  sincosq1sgn  25664  sincosq2sgn  25665  sincosq4sgn  25667  coseq00topi  25668  coseq0negpitopi  25669  tanabsge  25672  sinq12gt0  25673  cosq14gt0  25676  cos02pilt1  25691  cosq34lt1  25692  cosordlem  25695  cos0pilt1  25697  tanord1  25702  tanord  25703  tanregt0  25704  negpitopissre  25705  ellogrn  25724  logimclad  25737  argregt0  25774  argimgt0  25776  argimlt0  25777  dvloglem  25812  logf1o2  25814  efopnlem2  25821  isosctrlem1  25977  asinneg  26045  asinsinlem  26050  acoscos  26052  reasinsin  26055  atanlogsublem  26074  atantan  26082  atanbndlem  26084  atanbnd  26085  atan1  26087  dchrvmasumlem2  26655  dchrvmasumiflem1  26658  tgldimor  26872  upgrfi  27470  umgrislfupgrlem  27501  upgrewlkle2  27982  upgr2pthnlp  28109  nmoptrii  30465  nmopcoi  30466  sgnsgn  32524  chtvalz  32618  lfuhgr2  33089  usgrcyclgt2v  33102  acycgr2v  33121  cusgracyclt3v  33127  dnizeq0  34664  cnndvlem1  34726  bj-pinftyccb  35401  bj-minftyccb  35405  bj-pinftynminfty  35407  sin2h  35776  cos2h  35777  tan2h  35778  asindmre  35869  dvasin  35870  dvacos  35871  areacirclem1  35874  acos1half  40177  areaquad  41054  isosctrlem1ALT  42561  sineq0ALT  42564  itgsin0pilem1  43498  fourierdlem24  43679  fourierdlem38  43693  fourierdlem43  43698  fourierdlem44  43699  fourierdlem46  43700  fourierdlem62  43716  fourierdlem74  43728  fourierdlem75  43729  fourierdlem85  43739  fourierdlem88  43742  fourierdlem93  43747  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem112  43766  fourierdlem114  43768  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  fouriercn  43780  salexct2  43885  mod42tp1mod8  45065  bgoldbtbndlem1  45268  bgoldbtbnd  45272  pgrpgt2nabl  45713  sepfsepc  46232