Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rpre | Unicode version |
Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.) |
Ref | Expression |
---|---|
rpre |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rp 9410 | . . 3 | |
2 | ssrab2 3152 | . . 3 | |
3 | 1, 2 | eqsstri 3099 | . 2 |
4 | 3 | sseli 3063 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 crab 2397 class class class wbr 3899 cr 7587 cc0 7588 clt 7768 crp 9409 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-rab 2402 df-in 3047 df-ss 3054 df-rp 9410 |
This theorem is referenced by: rpxr 9417 rpcn 9418 rpssre 9420 rpge0 9422 rprege0 9424 rpap0 9426 rprene0 9427 rpreap0 9428 rpaddcl 9433 rpmulcl 9434 rpdivcl 9435 rpgecl 9438 ledivge1le 9481 addlelt 9523 iccdil 9749 expnlbnd 10384 caucvgre 10721 rennim 10742 rpsqrtcl 10781 qdenre 10942 rpmaxcl 10963 rpmincl 10977 xrminrpcl 11011 2clim 11038 cn1lem 11051 climsqz 11072 climsqz2 11073 climcau 11084 efgt1 11330 ef01bndlem 11390 bdmet 12598 bdmopn 12600 dveflem 12782 |
Copyright terms: Public domain | W3C validator |