Theorem rexri 8046

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

Syntax hints:   ∈ wcel 2160  ℝcr 7841  ℝ^*cxr 8022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-xr 8027

This theorem is referenced by:  1xr  8047  cos12dec  11810  halfleoddlt  11934  reeff1oleme  14670  reeff1o  14671  sin0pilem2  14680  neghalfpirx  14692  sincosq1sgn  14724  sincosq2sgn  14725  sincosq4sgn  14727  sinq12gt0  14728  cosq14gt0  14730  cosq23lt0  14731  coseq0q4123  14732  coseq00topi  14733  coseq0negpitopi  14734  cosordlem  14747  cosq34lt1  14748  cos02pilt1  14749  cos0pilt1  14750  ioocosf1o  14752  negpitopissre  14753  iooref1o  15261  taupi  15300