Theorem rpre 9885

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

Syntax hints:   → wi 4   ∈ wcel 2200  {crab 2512   class class class wbr 4086  ℝcr 8021  0cc0 8022   < clt 8204  ℝ⁺crp 9878

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 3204  df-ss 3211  df-rp 9879

This theorem is referenced by:  rpxr  9886  rpcn  9887  rpssre  9889  rpge0  9891  rprege0  9893  rpap0  9895  rprene0  9896  rpreap0  9897  rpaddcl  9902  rpmulcl  9903  rpdivcl  9904  rpgecl  9907  ledivge1le  9951  addlelt  9993  iccdil  10223  expnlbnd  10916  caucvgre  11532  rennim  11553  rpsqrtcl  11592  qdenre  11753  rpmaxcl  11774  rpmincl  11789  xrminrpcl  11825  2clim  11852  cn1lem  11865  climsqz  11886  climsqz2  11887  climcau  11898  efgt1  12248  ef01bndlem  12307  sinltxirr  12312  bdmet  15216  bdmopn  15218  dveflem  15440  reeff1o  15487  logleb  15589  logrpap0b  15590  cxple3  15635  rpcxpsqrt  15636  rpcxpsqrtth  15644  dceqnconst  16600  dcapnconst  16601