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 3198 | . . 3 | |
2 | eldifn 3199 | . . 3 | |
3 | 1, 2 | pm2.65i 628 | . 2 |
4 | df-nul 3364 | . . 3 | |
5 | 4 | eleq2i 2206 | . 2 |
6 | 3, 5 | mtbir 660 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wcel 1480 cvv 2686 cdif 3068 c0 3363 |
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-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 df-dif 3073 df-nul 3364 |
This theorem is referenced by: n0i 3368 n0rf 3375 rex0 3380 eq0 3381 abvor0dc 3386 rab0 3391 un0 3396 in0 3397 0ss 3401 disj 3411 ral0 3464 int0 3785 iun0 3869 0iun 3870 br0 3976 exmid01 4121 nlim0 4316 nsuceq0g 4340 ordtriexmidlem 4435 ordtriexmidlem2 4436 ordtriexmid 4437 ordtri2or2exmidlem 4441 onsucelsucexmidlem 4444 reg2exmidlema 4449 reg3exmidlemwe 4493 nn0eln0 4533 0xp 4619 dm0 4753 dm0rn0 4756 reldm0 4757 cnv0 4942 co02 5052 0fv 5456 acexmidlema 5765 acexmidlemb 5766 acexmidlemab 5768 mpo0 5841 nnsucelsuc 6387 nnsucuniel 6391 nnmordi 6412 nnaordex 6423 0er 6463 fidcenumlemrk 6842 elni2 7122 nlt1pig 7149 0npr 7291 fzm1 9880 frec2uzltd 10176 0tonninf 10212 sum0 11157 fsumsplit 11176 sumsplitdc 11201 fsum2dlemstep 11203 ennnfonelem1 11920 0ntop 12174 0met 12553 bdcnul 13063 bj-nnelirr 13151 nninfalllemn 13202 |
Copyright terms: Public domain | W3C validator |