Theorem rexri 11177

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

Syntax hints:   ∈ wcel 2113  ℝcr 11012  ℝ^*cxr 11152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-xr 11157

This theorem is referenced by:  1xr  11178  xnn0n0n1ge2b  13033  hashgt23el  14333  hashge2el2difr  14390  tanhbnd  16072  halfleoddlt  16275  oprpiece1res1  24877  oprpiece1res2  24878  pcoass  24952  vitalilem4  25540  neghalfpirx  26403  sincosq1sgn  26435  sincosq2sgn  26436  sincosq4sgn  26438  coseq00topi  26439  coseq0negpitopi  26440  tanabsge  26443  sinq12gt0  26444  cosq14gt0  26447  cos02pilt1  26463  cosq34lt1  26464  cosordlem  26467  cos0pilt1  26469  tanord1  26474  tanord  26475  tanregt0  26476  negpitopissre  26477  ellogrn  26496  logimclad  26509  argregt0  26547  argimgt0  26549  argimlt0  26550  dvloglem  26585  logf1o2  26587  efopnlem2  26594  isosctrlem1  26756  asinneg  26824  asinsinlem  26829  acoscos  26831  reasinsin  26834  atanlogsublem  26853  atantan  26861  atanbndlem  26863  atanbnd  26864  atan1  26866  dchrvmasumlem2  27437  dchrvmasumiflem1  27440  tgldimor  28481  upgrfi  29071  umgrislfupgrlem  29102  upgrewlkle2  29587  upgr2pthnlp  29712  nmoptrii  32076  nmopcoi  32077  sgnsgn  32829  rtelextdg2lem  33760  chtvalz  34663  lfuhgr2  35184  usgrcyclgt2v  35196  acycgr2v  35215  cusgracyclt3v  35221  dnizeq0  36540  cnndvlem1  36602  bj-pinftyccb  37286  bj-minftyccb  37290  bj-pinftynminfty  37292  sin2h  37670  cos2h  37671  tan2h  37672  asindmre  37763  dvasin  37764  dvacos  37765  areacirclem1  37768  acos1half  42476  areaquad  43333  isosctrlem1ALT  45050  sineq0ALT  45053  itgsin0pilem1  46072  fourierdlem24  46253  fourierdlem38  46267  fourierdlem43  46272  fourierdlem44  46273  fourierdlem46  46274  fourierdlem62  46290  fourierdlem74  46302  fourierdlem75  46303  fourierdlem85  46313  fourierdlem88  46316  fourierdlem93  46321  fourierdlem102  46330  fourierdlem103  46331  fourierdlem104  46332  fourierdlem111  46339  fourierdlem112  46340  fourierdlem114  46342  sqwvfoura  46350  sqwvfourb  46351  fourierswlem  46352  fouriersw  46353  fouriercn  46354  salexct2  46461  rehalfge1  47459  mod42tp1mod8  47726  bgoldbtbndlem1  47929  bgoldbtbnd  47933  pgrpgt2nabl  48490  sepfsepc  49052