Theorem rexri 11201

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

Syntax hints:   ∈ wcel 2119  ℝcr 11035  ℝ^*cxr 11176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-xr 11181

This theorem is referenced by:  1xr  11202  xnn0n0n1ge2b  13081  hashgt23el  14384  hashge2el2difr  14441  tanhbnd  16126  halfleoddlt  16329  oprpiece1res1  24943  oprpiece1res2  24944  pcoass  25016  vitalilem4  25603  neghalfpirx  26455  sincosq1sgn  26487  sincosq2sgn  26488  sincosq4sgn  26490  coseq00topi  26491  coseq0negpitopi  26492  tanabsge  26495  sinq12gt0  26496  cosq14gt0  26499  cos02pilt1  26515  cosq34lt1  26516  cosordlem  26519  cos0pilt1  26521  tanord1  26526  tanord  26527  tanregt0  26528  negpitopissre  26529  ellogrn  26548  logimclad  26561  argregt0  26599  argimgt0  26601  argimlt0  26602  dvloglem  26637  logf1o2  26639  efopnlem2  26646  isosctrlem1  26807  asinneg  26875  asinsinlem  26880  acoscos  26882  reasinsin  26885  atanlogsublem  26904  atantan  26912  atanbndlem  26914  atanbnd  26915  atan1  26917  dchrvmasumlem2  27486  dchrvmasumiflem1  27489  tgldimor  28595  upgrfi  29185  umgrislfupgrlem  29216  upgrewlkle2  29700  upgr2pthnlp  29825  nmoptrii  32190  nmopcoi  32191  sgnsgn  32940  rtelextdg2lem  33917  chtvalz  34820  lfuhgr2  35354  usgrcyclgt2v  35366  acycgr2v  35385  cusgracyclt3v  35391  dnizeq0  36788  cnndvlem1  36850  bj-pinftyccb  37588  bj-minftyccb  37592  bj-pinftynminfty  37594  sin2h  37984  cos2h  37985  tan2h  37986  asindmre  38077  dvasin  38078  dvacos  38079  areacirclem1  38082  acos1half  42842  areaquad  43668  isosctrlem1ALT  45384  sineq0ALT  45387  itgsin0pilem1  46400  fourierdlem24  46581  fourierdlem38  46595  fourierdlem43  46600  fourierdlem44  46601  fourierdlem46  46602  fourierdlem62  46618  fourierdlem74  46630  fourierdlem75  46631  fourierdlem85  46641  fourierdlem88  46644  fourierdlem93  46649  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  fourierdlem112  46668  fourierdlem114  46670  sqwvfoura  46678  sqwvfourb  46679  fourierswlem  46680  fouriersw  46681  fouriercn  46682  salexct2  46789  goldrapos  47353  rehalfge1  47809  mod42tp1mod8  48087  bgoldbtbndlem1  48303  bgoldbtbnd  48307  pgrpgt2nabl  48864  sepfsepc  49425