Theorem rexri 11394

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

This proof depends on syntax axioms:   ∈ wcel 2147  ℝcr 11226  ℝ^*cxr 11369

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-xr 11374

This theorem is used by:  1xr  11395  xnn0n0n1ge2b  13288  hashgt23el  14596  hashge2el2difr  14653  tanhbnd  16358  halfleoddlt  16561  oprpiece1res1  25302  oprpiece1res2  25303  pcoass  25375  vitalilem4  25962  neghalfpirx  26825  sincosq1sgn  26857  sincosq2sgn  26858  sincosq4sgn  26860  coseq00topi  26861  coseq0negpitopi  26862  tanabsge  26865  sinq12gt0  26866  cosq14gt0  26869  cos02pilt1  26884  cosq34lt1  26885  cosordlem  26888  cos0pilt1  26890  tanord1  26895  tanord  26896  tanregt0  26897  negpitopissre  26898  ellogrn  26917  logimclad  26930  argregt0  26968  argimgt0  26970  argimlt0  26971  dvloglem  27006  logf1o2  27008  efopnlem2  27015  isosctrlem1  27176  asinneg  27244  asinsinlem  27249  acoscos  27251  reasinsin  27254  atanlogsublem  27273  atantan  27281  atanbndlem  27283  atanbnd  27284  atan1  27286  dchrvmasumlem2  27855  dchrvmasumiflem1  27858  tgldimor  28995  upgrfi  29699  umgrislfupgrlem  29730  lfuhgr2  29757  upgrewlkle2  30217  upgr2pthnlp  30348  nmoptrii  32726  nmopcoi  32727  sgnsgn  33492  rtelextdg2lem  34428  chtvalz  35328  usgrcyclgt2v  36067  acycgr2v  36072  cusgracyclt3v  36078  dnizeq0  37519  cnndvlem1  37581  bj-pinftyccb  38334  bj-minftyccb  38338  bj-pinftynminfty  38340  sin2h  38725  cos2h  38726  tan2h  38727  asindmre  38813  dvasin  38814  dvacos  38815  areacirclem1  38818  acos1half  43602  areaquad  44410  isosctrlem1ALT  46107  sineq0ALT  46110  itgsin0pilem1  47165  fourierdlem24  47346  fourierdlem38  47360  fourierdlem43  47365  fourierdlem44  47366  fourierdlem46  47367  fourierdlem62  47383  fourierdlem74  47395  fourierdlem75  47396  fourierdlem85  47406  fourierdlem88  47409  fourierdlem93  47414  fourierdlem102  47423  fourierdlem103  47424  fourierdlem104  47425  fourierdlem111  47432  fourierdlem112  47433  fourierdlem114  47435  sqwvfoura  47443  sqwvfourb  47444  fourierswlem  47445  fouriersw  47446  fouriercn  47447  salexct2  47554  goldrapos  48135  rehalfge1  48614  mod42tp1mod8  48892  bgoldbtbndlem1  49108  bgoldbtbnd  49112  pgrpgt2nabl  49683  sepfsepc  50247