Theorem rexri 10856

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

Syntax hints:   ∈ wcel 2112  ℝcr 10693  ℝ^*cxr 10831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-in 3860  df-ss 3870  df-xr 10836

This theorem is referenced by:  1xr  10857  xnn0n0n1ge2b  12688  hashgt23el  13956  hashge2el2difr  14012  tanhbnd  15685  halfleoddlt  15886  oprpiece1res1  23802  oprpiece1res2  23803  pcoass  23875  vitalilem4  24462  neghalfpirx  25310  sincosq1sgn  25342  sincosq2sgn  25343  sincosq4sgn  25345  coseq00topi  25346  coseq0negpitopi  25347  tanabsge  25350  sinq12gt0  25351  cosq14gt0  25354  cos02pilt1  25369  cosq34lt1  25370  cosordlem  25373  cos0pilt1  25375  tanord1  25380  tanord  25381  tanregt0  25382  negpitopissre  25383  ellogrn  25402  logimclad  25415  argregt0  25452  argimgt0  25454  argimlt0  25455  dvloglem  25490  logf1o2  25492  efopnlem2  25499  isosctrlem1  25655  asinneg  25723  asinsinlem  25728  acoscos  25730  reasinsin  25733  atanlogsublem  25752  atantan  25760  atanbndlem  25762  atanbnd  25763  atan1  25765  dchrvmasumlem2  26333  dchrvmasumiflem1  26336  tgldimor  26547  upgrfi  27136  umgrislfupgrlem  27167  upgrewlkle2  27648  upgr2pthnlp  27773  nmoptrii  30129  nmopcoi  30130  sgnsgn  32181  chtvalz  32275  lfuhgr2  32747  usgrcyclgt2v  32760  acycgr2v  32779  cusgracyclt3v  32785  dnizeq0  34341  cnndvlem1  34403  bj-pinftyccb  35076  bj-minftyccb  35080  bj-pinftynminfty  35082  sin2h  35453  cos2h  35454  tan2h  35455  asindmre  35546  dvasin  35547  dvacos  35548  areacirclem1  35551  acos1half  39833  areaquad  40691  isosctrlem1ALT  42168  sineq0ALT  42171  itgsin0pilem1  43109  fourierdlem24  43290  fourierdlem38  43304  fourierdlem43  43309  fourierdlem44  43310  fourierdlem46  43311  fourierdlem62  43327  fourierdlem74  43339  fourierdlem75  43340  fourierdlem85  43350  fourierdlem88  43353  fourierdlem93  43358  fourierdlem102  43367  fourierdlem103  43368  fourierdlem104  43369  fourierdlem111  43376  fourierdlem112  43377  fourierdlem114  43379  sqwvfoura  43387  sqwvfourb  43388  fourierswlem  43389  fouriersw  43390  fouriercn  43391  salexct2  43496  mod42tp1mod8  44670  bgoldbtbndlem1  44873  bgoldbtbnd  44877  pgrpgt2nabl  45318  sepfsepc  45837