Theorem rexri 11319

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

Syntax hints:   ∈ wcel 2108  ℝcr 11154  ℝ^*cxr 11294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-xr 11299

This theorem is referenced by:  1xr  11320  xnn0n0n1ge2b  13174  hashgt23el  14463  hashge2el2difr  14520  tanhbnd  16197  halfleoddlt  16399  oprpiece1res1  24982  oprpiece1res2  24983  pcoass  25057  vitalilem4  25646  neghalfpirx  26508  sincosq1sgn  26540  sincosq2sgn  26541  sincosq4sgn  26543  coseq00topi  26544  coseq0negpitopi  26545  tanabsge  26548  sinq12gt0  26549  cosq14gt0  26552  cos02pilt1  26568  cosq34lt1  26569  cosordlem  26572  cos0pilt1  26574  tanord1  26579  tanord  26580  tanregt0  26581  negpitopissre  26582  ellogrn  26601  logimclad  26614  argregt0  26652  argimgt0  26654  argimlt0  26655  dvloglem  26690  logf1o2  26692  efopnlem2  26699  isosctrlem1  26861  asinneg  26929  asinsinlem  26934  acoscos  26936  reasinsin  26939  atanlogsublem  26958  atantan  26966  atanbndlem  26968  atanbnd  26969  atan1  26971  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  tgldimor  28510  upgrfi  29108  umgrislfupgrlem  29139  upgrewlkle2  29624  upgr2pthnlp  29752  nmoptrii  32113  nmopcoi  32114  rtelextdg2lem  33767  sgnsgn  34551  chtvalz  34644  lfuhgr2  35124  usgrcyclgt2v  35136  acycgr2v  35155  cusgracyclt3v  35161  dnizeq0  36476  cnndvlem1  36538  bj-pinftyccb  37222  bj-minftyccb  37226  bj-pinftynminfty  37228  sin2h  37617  cos2h  37618  tan2h  37619  asindmre  37710  dvasin  37711  dvacos  37712  areacirclem1  37715  acos1half  42388  areaquad  43228  isosctrlem1ALT  44954  sineq0ALT  44957  itgsin0pilem1  45965  fourierdlem24  46146  fourierdlem38  46160  fourierdlem43  46165  fourierdlem44  46166  fourierdlem46  46167  fourierdlem62  46183  fourierdlem74  46195  fourierdlem75  46196  fourierdlem85  46206  fourierdlem88  46209  fourierdlem93  46214  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  fourierdlem114  46235  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  fouriercn  46247  salexct2  46354  mod42tp1mod8  47589  bgoldbtbndlem1  47792  bgoldbtbnd  47796  pgrpgt2nabl  48282  sepfsepc  48825