Theorem rpre 9659

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

Syntax hints:   → wi 4   ∈ wcel 2148  {crab 2459   class class class wbr 4003  ℝcr 7809  0cc0 7810   < clt 7991  ℝ⁺crp 9652

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-in 3135  df-ss 3142  df-rp 9653

This theorem is referenced by:  rpxr  9660  rpcn  9661  rpssre  9663  rpge0  9665  rprege0  9667  rpap0  9669  rprene0  9670  rpreap0  9671  rpaddcl  9676  rpmulcl  9677  rpdivcl  9678  rpgecl  9681  ledivge1le  9725  addlelt  9767  iccdil  9997  expnlbnd  10644  caucvgre  10989  rennim  11010  rpsqrtcl  11049  qdenre  11210  rpmaxcl  11231  rpmincl  11245  xrminrpcl  11281  2clim  11308  cn1lem  11321  climsqz  11342  climsqz2  11343  climcau  11354  efgt1  11704  ef01bndlem  11763  bdmet  13972  bdmopn  13974  dveflem  14157  reeff1o  14164  logleb  14266  logrpap0b  14267  cxple3  14311  rpcxpsqrt  14312  rpcxpsqrtth  14320  dceqnconst  14777  dcapnconst  14778