Theorem rexri 11272

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

Syntax hints:   ∈ wcel 2107  ℝcr 11109  ℝ^*cxr 11247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-xr 11252

This theorem is referenced by:  1xr  11273  xnn0n0n1ge2b  13111  hashgt23el  14384  hashge2el2difr  14442  tanhbnd  16104  halfleoddlt  16305  oprpiece1res1  24467  oprpiece1res2  24468  pcoass  24540  vitalilem4  25128  neghalfpirx  25976  sincosq1sgn  26008  sincosq2sgn  26009  sincosq4sgn  26011  coseq00topi  26012  coseq0negpitopi  26013  tanabsge  26016  sinq12gt0  26017  cosq14gt0  26020  cos02pilt1  26035  cosq34lt1  26036  cosordlem  26039  cos0pilt1  26041  tanord1  26046  tanord  26047  tanregt0  26048  negpitopissre  26049  ellogrn  26068  logimclad  26081  argregt0  26118  argimgt0  26120  argimlt0  26121  dvloglem  26156  logf1o2  26158  efopnlem2  26165  isosctrlem1  26323  asinneg  26391  asinsinlem  26396  acoscos  26398  reasinsin  26401  atanlogsublem  26420  atantan  26428  atanbndlem  26430  atanbnd  26431  atan1  26433  dchrvmasumlem2  27001  dchrvmasumiflem1  27004  tgldimor  27753  upgrfi  28351  umgrislfupgrlem  28382  upgrewlkle2  28863  upgr2pthnlp  28989  nmoptrii  31347  nmopcoi  31348  sgnsgn  33547  chtvalz  33641  lfuhgr2  34109  usgrcyclgt2v  34122  acycgr2v  34141  cusgracyclt3v  34147  dnizeq0  35351  cnndvlem1  35413  bj-pinftyccb  36102  bj-minftyccb  36106  bj-pinftynminfty  36108  sin2h  36478  cos2h  36479  tan2h  36480  asindmre  36571  dvasin  36572  dvacos  36573  areacirclem1  36576  acos1half  41415  areaquad  41965  isosctrlem1ALT  43695  sineq0ALT  43698  itgsin0pilem1  44666  fourierdlem24  44847  fourierdlem38  44861  fourierdlem43  44866  fourierdlem44  44867  fourierdlem46  44868  fourierdlem62  44884  fourierdlem74  44896  fourierdlem75  44897  fourierdlem85  44907  fourierdlem88  44910  fourierdlem93  44915  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  fourierdlem112  44934  fourierdlem114  44936  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  fouriercn  44948  salexct2  45055  mod42tp1mod8  46270  bgoldbtbndlem1  46473  bgoldbtbnd  46477  pgrpgt2nabl  47042  sepfsepc  47560