![]() |
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 3203 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eldifn 3204 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | pm2.65i 629 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-nul 3369 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | eleq2i 2207 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | mtbir 661 |
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 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 df-dif 3078 df-nul 3369 |
This theorem is referenced by: n0i 3373 n0rf 3380 rex0 3385 eq0 3386 abvor0dc 3391 rab0 3396 un0 3401 in0 3402 0ss 3406 disj 3416 ral0 3469 int0 3793 iun0 3877 0iun 3878 br0 3984 exmid01 4129 nlim0 4324 nsuceq0g 4348 ordtriexmidlem 4443 ordtriexmidlem2 4444 ordtriexmid 4445 ordtri2or2exmidlem 4449 onsucelsucexmidlem 4452 reg2exmidlema 4457 reg3exmidlemwe 4501 nn0eln0 4541 0xp 4627 dm0 4761 dm0rn0 4764 reldm0 4765 cnv0 4950 co02 5060 0fv 5464 acexmidlema 5773 acexmidlemb 5774 acexmidlemab 5776 mpo0 5849 nnsucelsuc 6395 nnsucuniel 6399 nnmordi 6420 nnaordex 6431 0er 6471 fidcenumlemrk 6850 elni2 7146 nlt1pig 7173 0npr 7315 fzm1 9911 frec2uzltd 10207 0tonninf 10243 sum0 11189 fsumsplit 11208 sumsplitdc 11233 fsum2dlemstep 11235 ennnfonelem1 11956 0ntop 12213 0met 12592 bdcnul 13234 bj-nnelirr 13322 nninfalllemn 13377 |
Copyright terms: Public domain | W3C validator |