![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elnn | Unicode version |
Description: A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.) |
Ref | Expression |
---|---|
elnn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elomssom 4616 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ssel2 3162 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | ancoms 268 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylan2 286 |
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-in1 615 ax-in2 616 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-sep 4133 ax-nul 4141 ax-pow 4186 ax-pr 4221 ax-un 4445 ax-iinf 4599 |
This theorem depends on definitions: df-bi 117 df-3an 981 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ral 2470 df-rex 2471 df-v 2751 df-dif 3143 df-un 3145 df-in 3147 df-ss 3154 df-nul 3435 df-pw 3589 df-sn 3610 df-pr 3611 df-uni 3822 df-int 3857 df-suc 4383 df-iom 4602 |
This theorem is referenced by: ordom 4618 peano2b 4626 nntr2 6517 nndifsnid 6521 nnaordi 6522 nnmordi 6530 fidceq 6882 nnwetri 6928 enumctlemm 7126 nninfwlpoimlemg 7186 nninfwlpoimlemginf 7187 2onetap 7267 2omotaplemap 7269 ennnfonelemdm 12434 ennnfonelemnn0 12436 xpscf 12784 nnti 15016 nninfsellemdc 15031 nninfsellemeq 15035 nninfsellemeqinf 15037 |
Copyright terms: Public domain | W3C validator |