Theorem rexri 10499

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

Syntax hints:   ∈ wcel 2050  ℝcr 10334  ℝ^*cxr 10473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-v 3418  df-un 3835  df-in 3837  df-ss 3844  df-xr 10478

This theorem is referenced by:  1xr  10500  xnn0n0n1ge2b  12343  hashgt23el  13598  hashge2el2difr  13650  tanhbnd  15374  halfleoddlt  15571  oprpiece1res1  23258  oprpiece1res2  23259  pcoass  23331  vitalilem4  23915  neghalfpirx  24755  sincosq1sgn  24787  sincosq2sgn  24788  sincosq4sgn  24790  coseq00topi  24791  coseq0negpitopi  24792  tanabsge  24795  sinq12gt0  24796  cosq14gt0  24799  cosordlem  24816  tanord1  24822  tanord  24823  tanregt0  24824  negpitopissre  24825  ellogrn  24844  logimclad  24857  argregt0  24894  argimgt0  24896  argimlt0  24897  dvloglem  24932  logf1o2  24934  efopnlem2  24941  isosctrlem1  25097  asinneg  25165  asinsinlem  25170  acoscos  25172  reasinsin  25175  atanlogsublem  25194  atantan  25202  atanbndlem  25204  atanbnd  25205  atan1  25207  dchrvmasumlem2  25776  dchrvmasumiflem1  25779  tgldimor  25990  upgrfi  26579  umgrislfupgrlem  26610  upgrewlkle2  27091  upgr2pthnlp  27221  nmoptrii  29652  nmopcoi  29653  sgnsgn  31449  chtvalz  31545  dnizeq0  33331  cnndvlem1  33393  bj-pinftyccb  33969  bj-minftyccb  33973  bj-pinftynminfty  33975  sin2h  34320  cos2h  34321  tan2h  34322  asindmre  34415  dvasin  34416  dvacos  34417  areacirclem1  34420  areaquad  39216  isosctrlem1ALT  40684  sineq0ALT  40687  itgsin0pilem1  41663  fourierdlem24  41845  fourierdlem38  41859  fourierdlem43  41864  fourierdlem44  41865  fourierdlem46  41866  fourierdlem62  41882  fourierdlem74  41894  fourierdlem75  41895  fourierdlem85  41905  fourierdlem88  41908  fourierdlem93  41913  fourierdlem102  41922  fourierdlem103  41923  fourierdlem104  41924  fourierdlem111  41931  fourierdlem112  41932  fourierdlem114  41934  sqwvfoura  41942  sqwvfourb  41943  fourierswlem  41944  fouriersw  41945  fouriercn  41946  salexct2  42051  mod42tp1mod8  43133  bgoldbtbndlem1  43336  bgoldbtbnd  43340  pgrpgt2nabl  43778