Theorem rexri 11202

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-xr 11182

This theorem is referenced by:  1xr  11203  xnn0n0n1ge2b  13058  hashgt23el  14359  hashge2el2difr  14416  tanhbnd  16098  halfleoddlt  16301  oprpiece1res1  24917  oprpiece1res2  24918  pcoass  24992  vitalilem4  25580  neghalfpirx  26443  sincosq1sgn  26475  sincosq2sgn  26476  sincosq4sgn  26478  coseq00topi  26479  coseq0negpitopi  26480  tanabsge  26483  sinq12gt0  26484  cosq14gt0  26487  cos02pilt1  26503  cosq34lt1  26504  cosordlem  26507  cos0pilt1  26509  tanord1  26514  tanord  26515  tanregt0  26516  negpitopissre  26517  ellogrn  26536  logimclad  26549  argregt0  26587  argimgt0  26589  argimlt0  26590  dvloglem  26625  logf1o2  26627  efopnlem2  26634  isosctrlem1  26796  asinneg  26864  asinsinlem  26869  acoscos  26871  reasinsin  26874  atanlogsublem  26893  atantan  26901  atanbndlem  26903  atanbnd  26904  atan1  26906  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  tgldimor  28586  upgrfi  29176  umgrislfupgrlem  29207  upgrewlkle2  29692  upgr2pthnlp  29817  nmoptrii  32181  nmopcoi  32182  sgnsgn  32932  rtelextdg2lem  33903  chtvalz  34806  lfuhgr2  35332  usgrcyclgt2v  35344  acycgr2v  35363  cusgracyclt3v  35369  dnizeq0  36694  cnndvlem1  36756  bj-pinftyccb  37470  bj-minftyccb  37474  bj-pinftynminfty  37476  sin2h  37855  cos2h  37856  tan2h  37857  asindmre  37948  dvasin  37949  dvacos  37950  areacirclem1  37953  acos1half  42722  areaquad  43567  isosctrlem1ALT  45283  sineq0ALT  45286  itgsin0pilem1  46302  fourierdlem24  46483  fourierdlem38  46497  fourierdlem43  46502  fourierdlem44  46503  fourierdlem46  46504  fourierdlem62  46520  fourierdlem74  46532  fourierdlem75  46533  fourierdlem85  46543  fourierdlem88  46546  fourierdlem93  46551  fourierdlem102  46560  fourierdlem103  46561  fourierdlem104  46562  fourierdlem111  46569  fourierdlem112  46570  fourierdlem114  46572  sqwvfoura  46580  sqwvfourb  46581  fourierswlem  46582  fouriersw  46583  fouriercn  46584  salexct2  46691  rehalfge1  47689  mod42tp1mod8  47956  bgoldbtbndlem1  48159  bgoldbtbnd  48163  pgrpgt2nabl  48720  sepfsepc  49281