Theorem rexri 10964

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 10952	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ ℝ*

Syntax hints:   ∈ wcel 2108  ℝcr 10801  ℝ^*cxr 10939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-xr 10944

This theorem is referenced by:  1xr  10965  xnn0n0n1ge2b  12796  hashgt23el  14067  hashge2el2difr  14123  tanhbnd  15798  halfleoddlt  15999  oprpiece1res1  24020  oprpiece1res2  24021  pcoass  24093  vitalilem4  24680  neghalfpirx  25528  sincosq1sgn  25560  sincosq2sgn  25561  sincosq4sgn  25563  coseq00topi  25564  coseq0negpitopi  25565  tanabsge  25568  sinq12gt0  25569  cosq14gt0  25572  cos02pilt1  25587  cosq34lt1  25588  cosordlem  25591  cos0pilt1  25593  tanord1  25598  tanord  25599  tanregt0  25600  negpitopissre  25601  ellogrn  25620  logimclad  25633  argregt0  25670  argimgt0  25672  argimlt0  25673  dvloglem  25708  logf1o2  25710  efopnlem2  25717  isosctrlem1  25873  asinneg  25941  asinsinlem  25946  acoscos  25948  reasinsin  25951  atanlogsublem  25970  atantan  25978  atanbndlem  25980  atanbnd  25981  atan1  25983  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  tgldimor  26767  upgrfi  27364  umgrislfupgrlem  27395  upgrewlkle2  27876  upgr2pthnlp  28001  nmoptrii  30357  nmopcoi  30358  sgnsgn  32415  chtvalz  32509  lfuhgr2  32980  usgrcyclgt2v  32993  acycgr2v  33012  cusgracyclt3v  33018  dnizeq0  34582  cnndvlem1  34644  bj-pinftyccb  35319  bj-minftyccb  35323  bj-pinftynminfty  35325  sin2h  35694  cos2h  35695  tan2h  35696  asindmre  35787  dvasin  35788  dvacos  35789  areacirclem1  35792  acos1half  40098  areaquad  40963  isosctrlem1ALT  42443  sineq0ALT  42446  itgsin0pilem1  43381  fourierdlem24  43562  fourierdlem38  43576  fourierdlem43  43581  fourierdlem44  43582  fourierdlem46  43583  fourierdlem62  43599  fourierdlem74  43611  fourierdlem75  43612  fourierdlem85  43622  fourierdlem88  43625  fourierdlem93  43630  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  fourierdlem114  43651  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  fouriercn  43663  salexct2  43768  mod42tp1mod8  44942  bgoldbtbndlem1  45145  bgoldbtbnd  45149  pgrpgt2nabl  45590  sepfsepc  46109