![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rpre | GIF version |
Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.) |
Ref | Expression |
---|---|
rpre | ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rp 9672 | . . 3 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
2 | ssrab2 3255 | . . 3 ⊢ {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ | |
3 | 1, 2 | eqsstri 3202 | . 2 ⊢ ℝ+ ⊆ ℝ |
4 | 3 | sseli 3166 | 1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 {crab 2472 class class class wbr 4018 ℝcr 7828 0cc0 7829 < clt 8010 ℝ+crp 9671 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-rab 2477 df-in 3150 df-ss 3157 df-rp 9672 |
This theorem is referenced by: rpxr 9679 rpcn 9680 rpssre 9682 rpge0 9684 rprege0 9686 rpap0 9688 rprene0 9689 rpreap0 9690 rpaddcl 9695 rpmulcl 9696 rpdivcl 9697 rpgecl 9700 ledivge1le 9744 addlelt 9786 iccdil 10016 expnlbnd 10663 caucvgre 11008 rennim 11029 rpsqrtcl 11068 qdenre 11229 rpmaxcl 11250 rpmincl 11264 xrminrpcl 11300 2clim 11327 cn1lem 11340 climsqz 11361 climsqz2 11362 climcau 11373 efgt1 11723 ef01bndlem 11782 bdmet 14399 bdmopn 14401 dveflem 14584 reeff1o 14591 logleb 14693 logrpap0b 14694 cxple3 14738 rpcxpsqrt 14739 rpcxpsqrtth 14747 dceqnconst 15206 dcapnconst 15207 |
Copyright terms: Public domain | W3C validator |