Theorem rpre 9895

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 9889	. . 3 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
2		ssrab2 3312	. . 3 ⊢ {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ
3	1, 2	eqsstri 3259	. 2 ⊢ ℝ+ ⊆ ℝ
4	3	sseli 3223	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2202  {crab 2514   class class class wbr 4088  ℝcr 8031  0cc0 8032   < clt 8214  ℝ⁺crp 9888

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-in 3206  df-ss 3213  df-rp 9889

This theorem is referenced by:  rpxr  9896  rpcn  9897  rpssre  9899  rpge0  9901  rprege0  9903  rpap0  9905  rprene0  9906  rpreap0  9907  rpaddcl  9912  rpmulcl  9913  rpdivcl  9914  rpgecl  9917  ledivge1le  9961  addlelt  10003  iccdil  10233  expnlbnd  10927  caucvgre  11546  rennim  11567  rpsqrtcl  11606  qdenre  11767  rpmaxcl  11788  rpmincl  11803  xrminrpcl  11839  2clim  11866  cn1lem  11879  climsqz  11900  climsqz2  11901  climcau  11912  efgt1  12263  ef01bndlem  12322  sinltxirr  12327  bdmet  15232  bdmopn  15234  dveflem  15456  reeff1o  15503  logleb  15605  logrpap0b  15606  cxple3  15651  rpcxpsqrt  15652  rpcxpsqrtth  15660  dceqnconst  16691  dcapnconst  16692