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 ⊢ 𝐴 ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2145  ℝcr 11180  ℝ^*cxr 11323

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-xr 11328

This theorem is used by:  1xr  11349  xnn0n0n1ge2b  13242  hashgt23el  14549  hashge2el2difr  14606  tanhbnd  16309  halfleoddlt  16512  oprpiece1res1  25252  oprpiece1res2  25253  pcoass  25325  vitalilem4  25912  neghalfpirx  26777  sincosq1sgn  26809  sincosq2sgn  26810  sincosq4sgn  26812  coseq00topi  26813  coseq0negpitopi  26814  tanabsge  26817  sinq12gt0  26818  cosq14gt0  26821  cos02pilt1  26836  cosq34lt1  26837  cosordlem  26840  cos0pilt1  26842  tanord1  26847  tanord  26848  tanregt0  26849  negpitopissre  26850  ellogrn  26869  logimclad  26882  argregt0  26920  argimgt0  26922  argimlt0  26923  dvloglem  26958  logf1o2  26960  efopnlem2  26967  isosctrlem1  27128  asinneg  27196  asinsinlem  27201  acoscos  27203  reasinsin  27206  atanlogsublem  27225  atantan  27233  atanbndlem  27235  atanbnd  27236  atan1  27238  dchrvmasumlem2  27807  dchrvmasumiflem1  27810  tgldimor  28947  upgrfi  29651  umgrislfupgrlem  29682  lfuhgr2  29709  upgrewlkle2  30169  upgr2pthnlp  30300  nmoptrii  32678  nmopcoi  32679  sgnsgn  33404  rtelextdg2lem  34340  chtvalz  35241  usgrcyclgt2v  35879  acycgr2v  35884  cusgracyclt3v  35890  dnizeq0  37311  cnndvlem1  37373  bj-pinftyccb  38110  bj-minftyccb  38114  bj-pinftynminfty  38116  sin2h  38501  cos2h  38502  tan2h  38503  asindmre  38589  dvasin  38590  dvacos  38591  areacirclem1  38594  acos1half  43377  areaquad  44176  isosctrlem1ALT  45875  sineq0ALT  45878  itgsin0pilem1  46904  fourierdlem24  47085  fourierdlem38  47099  fourierdlem43  47104  fourierdlem44  47105  fourierdlem46  47106  fourierdlem62  47122  fourierdlem74  47134  fourierdlem75  47135  fourierdlem85  47145  fourierdlem88  47148  fourierdlem93  47153  fourierdlem102  47162  fourierdlem103  47163  fourierdlem104  47164  fourierdlem111  47171  fourierdlem112  47172  fourierdlem114  47174  sqwvfoura  47182  sqwvfourb  47183  fourierswlem  47184  fouriersw  47185  fouriercn  47186  salexct2  47293  goldrapos  47874  rehalfge1  48353  mod42tp1mod8  48631  bgoldbtbndlem1  48847  bgoldbtbnd  48851  pgrpgt2nabl  49422  sepfsepc  49980