Theorem rpre 9852

Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.)

Assertion

Ref	Expression
rpre	⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

Proof of Theorem rpre

Step	Hyp	Ref	Expression
1		df-rp 9846	. . 3 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
2		ssrab2 3309	. . 3 ⊢ {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ
3	1, 2	eqsstri 3256	. 2 ⊢ ℝ+ ⊆ ℝ
4	3	sseli 3220	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2200  {crab 2512   class class class wbr 4082  ℝcr 7994  0cc0 7995   < clt 8177  ℝ⁺crp 9845

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-in 3203  df-ss 3210  df-rp 9846

This theorem is referenced by:  rpxr  9853  rpcn  9854  rpssre  9856  rpge0  9858  rprege0  9860  rpap0  9862  rprene0  9863  rpreap0  9864  rpaddcl  9869  rpmulcl  9870  rpdivcl  9871  rpgecl  9874  ledivge1le  9918  addlelt  9960  iccdil  10190  expnlbnd  10881  caucvgre  11487  rennim  11508  rpsqrtcl  11547  qdenre  11708  rpmaxcl  11729  rpmincl  11744  xrminrpcl  11780  2clim  11807  cn1lem  11820  climsqz  11841  climsqz2  11842  climcau  11853  efgt1  12203  ef01bndlem  12262  sinltxirr  12267  bdmet  15170  bdmopn  15172  dveflem  15394  reeff1o  15441  logleb  15543  logrpap0b  15544  cxple3  15589  rpcxpsqrt  15590  rpcxpsqrtth  15598  dceqnconst  16387  dcapnconst  16388