Theorem rexri 11316

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

Syntax hints:   ∈ wcel 2105  ℝcr 11151  ℝ^*cxr 11291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-xr 11296

This theorem is referenced by:  1xr  11317  xnn0n0n1ge2b  13170  hashgt23el  14459  hashge2el2difr  14516  tanhbnd  16193  halfleoddlt  16395  oprpiece1res1  24995  oprpiece1res2  24996  pcoass  25070  vitalilem4  25659  neghalfpirx  26522  sincosq1sgn  26554  sincosq2sgn  26555  sincosq4sgn  26557  coseq00topi  26558  coseq0negpitopi  26559  tanabsge  26562  sinq12gt0  26563  cosq14gt0  26566  cos02pilt1  26582  cosq34lt1  26583  cosordlem  26586  cos0pilt1  26588  tanord1  26593  tanord  26594  tanregt0  26595  negpitopissre  26596  ellogrn  26615  logimclad  26628  argregt0  26666  argimgt0  26668  argimlt0  26669  dvloglem  26704  logf1o2  26706  efopnlem2  26713  isosctrlem1  26875  asinneg  26943  asinsinlem  26948  acoscos  26950  reasinsin  26953  atanlogsublem  26972  atantan  26980  atanbndlem  26982  atanbnd  26983  atan1  26985  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  tgldimor  28524  upgrfi  29122  umgrislfupgrlem  29153  upgrewlkle2  29638  upgr2pthnlp  29764  nmoptrii  32122  nmopcoi  32123  rtelextdg2lem  33731  sgnsgn  34529  chtvalz  34622  lfuhgr2  35102  usgrcyclgt2v  35115  acycgr2v  35134  cusgracyclt3v  35140  dnizeq0  36457  cnndvlem1  36519  bj-pinftyccb  37203  bj-minftyccb  37207  bj-pinftynminfty  37209  sin2h  37596  cos2h  37597  tan2h  37598  asindmre  37689  dvasin  37690  dvacos  37691  areacirclem1  37694  acos1half  42366  areaquad  43204  isosctrlem1ALT  44931  sineq0ALT  44934  itgsin0pilem1  45905  fourierdlem24  46086  fourierdlem38  46100  fourierdlem43  46105  fourierdlem44  46106  fourierdlem46  46107  fourierdlem62  46123  fourierdlem74  46135  fourierdlem75  46136  fourierdlem85  46146  fourierdlem88  46149  fourierdlem93  46154  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  fourierdlem114  46175  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  fouriercn  46187  salexct2  46294  mod42tp1mod8  47526  bgoldbtbndlem1  47729  bgoldbtbnd  47733  pgrpgt2nabl  48210  sepfsepc  48723