Theorem rexri 11348

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

Syntax hints:   ∈ wcel 2108  ℝcr 11183  ℝ^*cxr 11323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-xr 11328

This theorem is referenced by:  1xr  11349  xnn0n0n1ge2b  13194  hashgt23el  14473  hashge2el2difr  14530  tanhbnd  16209  halfleoddlt  16410  oprpiece1res1  25001  oprpiece1res2  25002  pcoass  25076  vitalilem4  25665  neghalfpirx  26526  sincosq1sgn  26558  sincosq2sgn  26559  sincosq4sgn  26561  coseq00topi  26562  coseq0negpitopi  26563  tanabsge  26566  sinq12gt0  26567  cosq14gt0  26570  cos02pilt1  26586  cosq34lt1  26587  cosordlem  26590  cos0pilt1  26592  tanord1  26597  tanord  26598  tanregt0  26599  negpitopissre  26600  ellogrn  26619  logimclad  26632  argregt0  26670  argimgt0  26672  argimlt0  26673  dvloglem  26708  logf1o2  26710  efopnlem2  26717  isosctrlem1  26879  asinneg  26947  asinsinlem  26952  acoscos  26954  reasinsin  26957  atanlogsublem  26976  atantan  26984  atanbndlem  26986  atanbnd  26987  atan1  26989  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  tgldimor  28528  upgrfi  29126  umgrislfupgrlem  29157  upgrewlkle2  29642  upgr2pthnlp  29768  nmoptrii  32126  nmopcoi  32127  rtelextdg2lem  33717  sgnsgn  34513  chtvalz  34606  lfuhgr2  35086  usgrcyclgt2v  35099  acycgr2v  35118  cusgracyclt3v  35124  dnizeq0  36441  cnndvlem1  36503  bj-pinftyccb  37187  bj-minftyccb  37191  bj-pinftynminfty  37193  sin2h  37570  cos2h  37571  tan2h  37572  asindmre  37663  dvasin  37664  dvacos  37665  areacirclem1  37668  acos1half  42340  areaquad  43177  isosctrlem1ALT  44905  sineq0ALT  44908  itgsin0pilem1  45871  fourierdlem24  46052  fourierdlem38  46066  fourierdlem43  46071  fourierdlem44  46072  fourierdlem46  46073  fourierdlem62  46089  fourierdlem74  46101  fourierdlem75  46102  fourierdlem85  46112  fourierdlem88  46115  fourierdlem93  46120  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  fourierdlem114  46141  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  fouriercn  46153  salexct2  46260  mod42tp1mod8  47476  bgoldbtbndlem1  47679  bgoldbtbnd  47683  pgrpgt2nabl  48091  sepfsepc  48607