![]() |
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 7923 |
. 2
![]() ![]() ![]() ![]() | |
2 | nnsscn 8910 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | ssexi 4138 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-sep 4118 ax-cnex 7890 ax-resscn 7891 ax-1re 7893 ax-addrcl 7896 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-v 2739 df-in 3135 df-ss 3142 df-int 3843 df-inn 8906 |
This theorem is referenced by: nn0ex 9168 nn0ennn 10416 climrecvg1n 11337 climcvg1nlem 11338 divcnv 11486 trireciplem 11489 expcnvap0 11491 expcnv 11493 geo2lim 11505 prmex 12093 qnumval 12165 qdenval 12166 oddennn 12373 evenennn 12374 xpnnen 12375 znnen 12379 qnnen 12412 ssnnctlemct 12427 nninfdc 12434 ndxarg 12465 trilpo 14440 redcwlpo 14452 nconstwlpo 14462 neapmkv 14464 |
Copyright terms: Public domain | W3C validator |