Theorem rexri 11268

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

Syntax hints:   ∈ wcel 2143  ℝcr 11100  ℝ^*cxr 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-xr 11248

This theorem is referenced by:  1xr  11269  xnn0n0n1ge2b  13158  hashgt23el  14463  hashge2el2difr  14520  tanhbnd  16218  halfleoddlt  16421  oprpiece1res1  25091  oprpiece1res2  25092  pcoass  25164  vitalilem4  25751  neghalfpirx  26609  sincosq1sgn  26641  sincosq2sgn  26642  sincosq4sgn  26644  coseq00topi  26645  coseq0negpitopi  26646  tanabsge  26649  sinq12gt0  26650  cosq14gt0  26653  cos02pilt1  26669  cosq34lt1  26670  cosordlem  26673  cos0pilt1  26675  tanord1  26680  tanord  26681  tanregt0  26682  negpitopissre  26683  ellogrn  26702  logimclad  26715  argregt0  26753  argimgt0  26755  argimlt0  26756  dvloglem  26791  logf1o2  26793  efopnlem2  26800  isosctrlem1  26961  asinneg  27029  asinsinlem  27034  acoscos  27036  reasinsin  27039  atanlogsublem  27058  atantan  27066  atanbndlem  27068  atanbnd  27069  atan1  27071  dchrvmasumlem2  27640  dchrvmasumiflem1  27643  tgldimor  28749  upgrfi  29419  umgrislfupgrlem  29450  upgrewlkle2  29934  upgr2pthnlp  30059  nmoptrii  32424  nmopcoi  32425  sgnsgn  33153  rtelextdg2lem  34094  chtvalz  34994  lfuhgr2  35589  usgrcyclgt2v  35601  acycgr2v  35620  cusgracyclt3v  35626  dnizeq0  37042  cnndvlem1  37104  bj-pinftyccb  37843  bj-minftyccb  37847  bj-pinftynminfty  37849  sin2h  38239  cos2h  38240  tan2h  38241  asindmre  38332  dvasin  38333  dvacos  38334  areacirclem1  38337  acos1half  43097  areaquad  43923  isosctrlem1ALT  45622  sineq0ALT  45625  itgsin0pilem1  46644  fourierdlem24  46825  fourierdlem38  46839  fourierdlem43  46844  fourierdlem44  46845  fourierdlem46  46846  fourierdlem62  46862  fourierdlem74  46874  fourierdlem75  46875  fourierdlem85  46885  fourierdlem88  46888  fourierdlem93  46893  fourierdlem102  46902  fourierdlem103  46903  fourierdlem104  46904  fourierdlem111  46911  fourierdlem112  46912  fourierdlem114  46914  sqwvfoura  46922  sqwvfourb  46923  fourierswlem  46924  fouriersw  46925  fouriercn  46926  salexct2  47033  goldrapos  47597  rehalfge1  48053  mod42tp1mod8  48331  bgoldbtbndlem1  48547  bgoldbtbnd  48551  pgrpgt2nabl  49123  sepfsepc  49683