![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nnex | Unicode version |
Description: The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
nnex |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 7998 |
. 2
![]() ![]() ![]() ![]() | |
2 | nnsscn 8989 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | ssexi 4168 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 2175 ax-sep 4148 ax-cnex 7965 ax-resscn 7966 ax-1re 7968 ax-addrcl 7971 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ral 2477 df-v 2762 df-in 3160 df-ss 3167 df-int 3872 df-inn 8985 |
This theorem is referenced by: nn0ex 9249 nn0ennn 10507 climrecvg1n 11494 climcvg1nlem 11495 divcnv 11643 trireciplem 11646 expcnvap0 11648 expcnv 11650 geo2lim 11662 prmex 12254 qnumval 12326 qdenval 12327 oddennn 12552 evenennn 12553 xpnnen 12554 znnen 12558 qnnen 12591 ssnnctlemct 12606 nninfdc 12613 ndxarg 12644 mulgnngsum 13200 trilpo 15603 redcwlpo 15615 nconstwlpo 15626 neapmkv 15628 |
Copyright terms: Public domain | W3C validator |