Theorem rexri 10699

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

Syntax hints:   ∈ wcel 2114  ℝcr 10536  ℝ^*cxr 10674

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-xr 10679

This theorem is referenced by:  1xr  10700  xnn0n0n1ge2b  12527  hashgt23el  13786  hashge2el2difr  13840  tanhbnd  15514  halfleoddlt  15711  oprpiece1res1  23555  oprpiece1res2  23556  pcoass  23628  vitalilem4  24212  neghalfpirx  25052  sincosq1sgn  25084  sincosq2sgn  25085  sincosq4sgn  25087  coseq00topi  25088  coseq0negpitopi  25089  tanabsge  25092  sinq12gt0  25093  cosq14gt0  25096  cos02pilt1  25111  cosq34lt1  25112  cosordlem  25115  tanord1  25121  tanord  25122  tanregt0  25123  negpitopissre  25124  ellogrn  25143  logimclad  25156  argregt0  25193  argimgt0  25195  argimlt0  25196  dvloglem  25231  logf1o2  25233  efopnlem2  25240  isosctrlem1  25396  asinneg  25464  asinsinlem  25469  acoscos  25471  reasinsin  25474  atanlogsublem  25493  atantan  25501  atanbndlem  25503  atanbnd  25504  atan1  25506  dchrvmasumlem2  26074  dchrvmasumiflem1  26077  tgldimor  26288  upgrfi  26876  umgrislfupgrlem  26907  upgrewlkle2  27388  upgr2pthnlp  27513  nmoptrii  29871  nmopcoi  29872  sgnsgn  31806  chtvalz  31900  lfuhgr2  32365  usgrcyclgt2v  32378  acycgr2v  32397  cusgracyclt3v  32403  dnizeq0  33814  cnndvlem1  33876  bj-pinftyccb  34506  bj-minftyccb  34510  bj-pinftynminfty  34512  sin2h  34897  cos2h  34898  tan2h  34899  asindmre  34992  dvasin  34993  dvacos  34994  areacirclem1  34997  areaquad  39843  isosctrlem1ALT  41288  sineq0ALT  41291  itgsin0pilem1  42255  fourierdlem24  42436  fourierdlem38  42450  fourierdlem43  42455  fourierdlem44  42456  fourierdlem46  42457  fourierdlem62  42473  fourierdlem74  42485  fourierdlem75  42486  fourierdlem85  42496  fourierdlem88  42499  fourierdlem93  42504  fourierdlem102  42513  fourierdlem103  42514  fourierdlem104  42515  fourierdlem111  42522  fourierdlem112  42523  fourierdlem114  42525  sqwvfoura  42533  sqwvfourb  42534  fourierswlem  42535  fouriersw  42536  fouriercn  42537  salexct2  42642  mod42tp1mod8  43787  bgoldbtbndlem1  43990  bgoldbtbnd  43994  pgrpgt2nabl  44434