ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rpre GIF version

Theorem rpre 8687
Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.)
Assertion
Ref Expression
rpre (𝐴 ∈ ℝ+𝐴 ∈ ℝ)

Proof of Theorem rpre
StepHypRef Expression
1 df-rp 8682 . . 3 + = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
2 ssrab2 3053 . . 3 {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ
31, 2eqsstri 3003 . 2 + ⊆ ℝ
43sseli 2969 1 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  {crab 2327   class class class wbr 3792  cr 6946  0cc0 6947   < clt 7119  +crp 8681
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rab 2332  df-in 2952  df-ss 2959  df-rp 8682
This theorem is referenced by:  rpxr  8688  rpcn  8689  rpssre  8691  rpge0  8693  rprege0  8695  rpap0  8697  rprene0  8698  rpreap0  8699  rpaddcl  8704  rpmulcl  8705  rpdivcl  8706  rpgecl  8709  ledivge1le  8750  addlelt  8786  iccdil  8967  expnlbnd  9541  caucvgre  9808  rennim  9829  rpsqrtcl  9868  qdenre  10029  2clim  10053  cn1lem  10065  climsqz  10086  climsqz2  10087  climcau  10097
  Copyright terms: Public domain W3C validator