Theorem rexri 11322

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

Syntax hints:   ∈ wcel 2099  ℝcr 11157  ℝ^*cxr 11297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3952  df-ss 3964  df-xr 11302

This theorem is referenced by:  1xr  11323  xnn0n0n1ge2b  13165  hashgt23el  14441  hashge2el2difr  14500  tanhbnd  16163  halfleoddlt  16364  oprpiece1res1  24967  oprpiece1res2  24968  pcoass  25042  vitalilem4  25631  neghalfpirx  26494  sincosq1sgn  26526  sincosq2sgn  26527  sincosq4sgn  26529  coseq00topi  26530  coseq0negpitopi  26531  tanabsge  26534  sinq12gt0  26535  cosq14gt0  26538  cos02pilt1  26553  cosq34lt1  26554  cosordlem  26557  cos0pilt1  26559  tanord1  26564  tanord  26565  tanregt0  26566  negpitopissre  26567  ellogrn  26586  logimclad  26599  argregt0  26637  argimgt0  26639  argimlt0  26640  dvloglem  26675  logf1o2  26677  efopnlem2  26684  isosctrlem1  26846  asinneg  26914  asinsinlem  26919  acoscos  26921  reasinsin  26924  atanlogsublem  26943  atantan  26951  atanbndlem  26953  atanbnd  26954  atan1  26956  dchrvmasumlem2  27527  dchrvmasumiflem1  27530  tgldimor  28429  upgrfi  29027  umgrislfupgrlem  29058  upgrewlkle2  29543  upgr2pthnlp  29669  nmoptrii  32027  nmopcoi  32028  rtelextdg2lem  33604  sgnsgn  34382  chtvalz  34475  lfuhgr2  34946  usgrcyclgt2v  34959  acycgr2v  34978  cusgracyclt3v  34984  dnizeq0  36178  cnndvlem1  36240  bj-pinftyccb  36928  bj-minftyccb  36932  bj-pinftynminfty  36934  sin2h  37311  cos2h  37312  tan2h  37313  asindmre  37404  dvasin  37405  dvacos  37406  areacirclem1  37409  acos1half  42328  areaquad  42881  isosctrlem1ALT  44610  sineq0ALT  44613  itgsin0pilem1  45571  fourierdlem24  45752  fourierdlem38  45766  fourierdlem43  45771  fourierdlem44  45772  fourierdlem46  45773  fourierdlem62  45789  fourierdlem74  45801  fourierdlem75  45802  fourierdlem85  45812  fourierdlem88  45815  fourierdlem93  45820  fourierdlem102  45829  fourierdlem103  45830  fourierdlem104  45831  fourierdlem111  45838  fourierdlem112  45839  fourierdlem114  45841  sqwvfoura  45849  sqwvfourb  45850  fourierswlem  45851  fouriersw  45852  fouriercn  45853  salexct2  45960  mod42tp1mod8  47174  bgoldbtbndlem1  47377  bgoldbtbnd  47381  pgrpgt2nabl  47745  sepfsepc  48261