![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > noel | Unicode version |
Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
Ref | Expression |
---|---|
noel |
![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifi 3257 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eldifn 3258 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | pm2.65i 639 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-nul 3423 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | eleq2i 2244 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | mtbir 671 |
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 614 ax-in2 615 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 |
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-v 2739 df-dif 3131 df-nul 3423 |
This theorem is referenced by: nel02 3427 n0i 3428 n0rf 3435 rex0 3440 eq0 3441 abvor0dc 3446 rab0 3451 un0 3456 in0 3457 0ss 3461 disj 3471 ral0 3524 int0 3858 iun0 3943 0iun 3944 br0 4051 exmid01 4198 nlim0 4394 nsuceq0g 4418 ordtriexmidlem 4518 ordtriexmidlem2 4519 ordtriexmid 4520 ontriexmidim 4521 ordtri2or2exmidlem 4525 onsucelsucexmidlem 4528 reg2exmidlema 4533 reg3exmidlemwe 4578 nn0eln0 4619 0xp 4706 dm0 4841 dm0rn0 4844 reldm0 4845 cnv0 5032 co02 5142 0fv 5550 acexmidlema 5865 acexmidlemb 5866 acexmidlemab 5868 mpo0 5944 nnsucelsuc 6491 nnsucuniel 6495 nnmordi 6516 nnaordex 6528 0er 6568 fidcenumlemrk 6952 nnnninfeq 7125 elni2 7312 nlt1pig 7339 0npr 7481 fzm1 10097 frec2uzltd 10400 0tonninf 10436 sum0 11391 fsumsplit 11410 sumsplitdc 11435 fsum2dlemstep 11437 prod0 11588 fprod2dlemstep 11625 ennnfonelem1 12402 0g0 12749 0ntop 13398 0met 13777 lgsdir2lem3 14324 if0ab 14439 bdcnul 14499 bj-nnelirr 14587 |
Copyright terms: Public domain | W3C validator |