Theorem rexri 11190

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

Syntax hints:   ∈ wcel 2113  ℝcr 11025  ℝ^*cxr 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-xr 11170

This theorem is referenced by:  1xr  11191  xnn0n0n1ge2b  13046  hashgt23el  14347  hashge2el2difr  14404  tanhbnd  16086  halfleoddlt  16289  oprpiece1res1  24905  oprpiece1res2  24906  pcoass  24980  vitalilem4  25568  neghalfpirx  26431  sincosq1sgn  26463  sincosq2sgn  26464  sincosq4sgn  26466  coseq00topi  26467  coseq0negpitopi  26468  tanabsge  26471  sinq12gt0  26472  cosq14gt0  26475  cos02pilt1  26491  cosq34lt1  26492  cosordlem  26495  cos0pilt1  26497  tanord1  26502  tanord  26503  tanregt0  26504  negpitopissre  26505  ellogrn  26524  logimclad  26537  argregt0  26575  argimgt0  26577  argimlt0  26578  dvloglem  26613  logf1o2  26615  efopnlem2  26622  isosctrlem1  26784  asinneg  26852  asinsinlem  26857  acoscos  26859  reasinsin  26862  atanlogsublem  26881  atantan  26889  atanbndlem  26891  atanbnd  26892  atan1  26894  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  tgldimor  28574  upgrfi  29164  umgrislfupgrlem  29195  upgrewlkle2  29680  upgr2pthnlp  29805  nmoptrii  32169  nmopcoi  32170  sgnsgn  32922  rtelextdg2lem  33883  chtvalz  34786  lfuhgr2  35313  usgrcyclgt2v  35325  acycgr2v  35344  cusgracyclt3v  35350  dnizeq0  36675  cnndvlem1  36737  bj-pinftyccb  37422  bj-minftyccb  37426  bj-pinftynminfty  37428  sin2h  37807  cos2h  37808  tan2h  37809  asindmre  37900  dvasin  37901  dvacos  37902  areacirclem1  37905  acos1half  42609  areaquad  43454  isosctrlem1ALT  45170  sineq0ALT  45173  itgsin0pilem1  46190  fourierdlem24  46371  fourierdlem38  46385  fourierdlem43  46390  fourierdlem44  46391  fourierdlem46  46392  fourierdlem62  46408  fourierdlem74  46420  fourierdlem75  46421  fourierdlem85  46431  fourierdlem88  46434  fourierdlem93  46439  fourierdlem102  46448  fourierdlem103  46449  fourierdlem104  46450  fourierdlem111  46457  fourierdlem112  46458  fourierdlem114  46460  sqwvfoura  46468  sqwvfourb  46469  fourierswlem  46470  fouriersw  46471  fouriercn  46472  salexct2  46579  rehalfge1  47577  mod42tp1mod8  47844  bgoldbtbndlem1  48047  bgoldbtbnd  48051  pgrpgt2nabl  48608  sepfsepc  49169