Theorem rexri 11203

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

Syntax hints:   ∈ wcel 2114  ℝcr 11037  ℝ^*cxr 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-xr 11183

This theorem is referenced by:  1xr  11204  xnn0n0n1ge2b  13083  hashgt23el  14386  hashge2el2difr  14443  tanhbnd  16128  halfleoddlt  16331  oprpiece1res1  24918  oprpiece1res2  24919  pcoass  24991  vitalilem4  25578  neghalfpirx  26430  sincosq1sgn  26462  sincosq2sgn  26463  sincosq4sgn  26465  coseq00topi  26466  coseq0negpitopi  26467  tanabsge  26470  sinq12gt0  26471  cosq14gt0  26474  cos02pilt1  26490  cosq34lt1  26491  cosordlem  26494  cos0pilt1  26496  tanord1  26501  tanord  26502  tanregt0  26503  negpitopissre  26504  ellogrn  26523  logimclad  26536  argregt0  26574  argimgt0  26576  argimlt0  26577  dvloglem  26612  logf1o2  26614  efopnlem2  26621  isosctrlem1  26782  asinneg  26850  asinsinlem  26855  acoscos  26857  reasinsin  26860  atanlogsublem  26879  atantan  26887  atanbndlem  26889  atanbnd  26890  atan1  26892  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  tgldimor  28570  upgrfi  29160  umgrislfupgrlem  29191  upgrewlkle2  29675  upgr2pthnlp  29800  nmoptrii  32165  nmopcoi  32166  sgnsgn  32914  rtelextdg2lem  33870  chtvalz  34773  lfuhgr2  35301  usgrcyclgt2v  35313  acycgr2v  35332  cusgracyclt3v  35338  dnizeq0  36735  cnndvlem1  36797  bj-pinftyccb  37535  bj-minftyccb  37539  bj-pinftynminfty  37541  sin2h  37931  cos2h  37932  tan2h  37933  asindmre  38024  dvasin  38025  dvacos  38026  areacirclem1  38029  acos1half  42790  areaquad  43644  isosctrlem1ALT  45360  sineq0ALT  45363  itgsin0pilem1  46378  fourierdlem24  46559  fourierdlem38  46573  fourierdlem43  46578  fourierdlem44  46579  fourierdlem46  46580  fourierdlem62  46596  fourierdlem74  46608  fourierdlem75  46609  fourierdlem85  46619  fourierdlem88  46622  fourierdlem93  46627  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fourierdlem114  46648  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  fouriercn  46660  salexct2  46767  goldrapos  47331  rehalfge1  47787  mod42tp1mod8  48065  bgoldbtbndlem1  48281  bgoldbtbnd  48285  pgrpgt2nabl  48842  sepfsepc  49403