Theorem rexri 11167

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

Syntax hints:   ∈ wcel 2111  ℝcr 11002  ℝ^*cxr 11142

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919  df-xr 11147

This theorem is referenced by:  1xr  11168  xnn0n0n1ge2b  13028  hashgt23el  14328  hashge2el2difr  14385  tanhbnd  16067  halfleoddlt  16270  oprpiece1res1  24874  oprpiece1res2  24875  pcoass  24949  vitalilem4  25537  neghalfpirx  26400  sincosq1sgn  26432  sincosq2sgn  26433  sincosq4sgn  26435  coseq00topi  26436  coseq0negpitopi  26437  tanabsge  26440  sinq12gt0  26441  cosq14gt0  26444  cos02pilt1  26460  cosq34lt1  26461  cosordlem  26464  cos0pilt1  26466  tanord1  26471  tanord  26472  tanregt0  26473  negpitopissre  26474  ellogrn  26493  logimclad  26506  argregt0  26544  argimgt0  26546  argimlt0  26547  dvloglem  26582  logf1o2  26584  efopnlem2  26591  isosctrlem1  26753  asinneg  26821  asinsinlem  26826  acoscos  26828  reasinsin  26831  atanlogsublem  26850  atantan  26858  atanbndlem  26860  atanbnd  26861  atan1  26863  dchrvmasumlem2  27434  dchrvmasumiflem1  27437  tgldimor  28478  upgrfi  29067  umgrislfupgrlem  29098  upgrewlkle2  29583  upgr2pthnlp  29708  nmoptrii  32069  nmopcoi  32070  sgnsgn  32819  rtelextdg2lem  33734  chtvalz  34637  lfuhgr2  35151  usgrcyclgt2v  35163  acycgr2v  35182  cusgracyclt3v  35188  dnizeq0  36508  cnndvlem1  36570  bj-pinftyccb  37254  bj-minftyccb  37258  bj-pinftynminfty  37260  sin2h  37649  cos2h  37650  tan2h  37651  asindmre  37742  dvasin  37743  dvacos  37744  areacirclem1  37747  acos1half  42390  areaquad  43248  isosctrlem1ALT  44965  sineq0ALT  44968  itgsin0pilem1  45987  fourierdlem24  46168  fourierdlem38  46182  fourierdlem43  46187  fourierdlem44  46188  fourierdlem46  46189  fourierdlem62  46205  fourierdlem74  46217  fourierdlem75  46218  fourierdlem85  46228  fourierdlem88  46231  fourierdlem93  46236  fourierdlem102  46245  fourierdlem103  46246  fourierdlem104  46247  fourierdlem111  46254  fourierdlem112  46255  fourierdlem114  46257  sqwvfoura  46265  sqwvfourb  46266  fourierswlem  46267  fouriersw  46268  fouriercn  46269  salexct2  46376  rehalfge1  47365  mod42tp1mod8  47632  bgoldbtbndlem1  47835  bgoldbtbnd  47839  pgrpgt2nabl  48396  sepfsepc  48958