Theorem rpre 8589

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

Syntax hints:   → wi 4   ∈ wcel 1393  {crab 2310   class class class wbr 3764  ℝcr 6888  0cc0 6889   < clt 7060  ℝ⁺crp 8583

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rab 2315  df-in 2924  df-ss 2931  df-rp 8584

This theorem is referenced by:  rpxr  8590  rpcn  8591  rpssre  8593  rpge0  8595  rprege0  8597  rpap0  8599  rprene0  8600  rpreap0  8601  rpaddcl  8606  rpmulcl  8607  rpdivcl  8608  rpgecl  8611  ledivge1le  8652  iccdil  8866  expnlbnd  9373  caucvgre  9580  rennim  9600  rpsqrtcl  9639  qdenre  9798  2clim  9822  cn1lem  9834  climsqz  9855  climsqz2  9856  climcau  9866