| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 0elon | Unicode version | ||
| Description: The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.) |
| Ref | Expression |
|---|---|
| 0elon |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ord0 4514 |
. 2
| |
| 2 | 0ex 4239 |
. . 3
| |
| 3 | 2 | elon 4497 |
. 2
|
| 4 | 1, 3 | mpbir 146 |
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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-ext 2216 ax-nul 4238 |
| This theorem depends on definitions: df-bi 117 df-tru 1401 df-nf 1510 df-sb 1812 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ral 2527 df-rex 2528 df-v 2817 df-dif 3215 df-in 3219 df-ss 3226 df-nul 3511 df-pw 3673 df-uni 3917 df-tr 4211 df-iord 4489 df-on 4491 |
| This theorem is referenced by: inton 4516 onn0 4523 onm 4524 limon 4637 ordtriexmid 4645 ontriexmidim 4646 ordtri2orexmid 4647 onsucsssucexmid 4651 onsucelsucexmid 4654 ordsoexmid 4686 ordpwsucexmid 4694 ordtri2or2exmid 4695 ontri2orexmidim 4696 tfr0dm 6555 1on 6656 ordgt0ge1 6670 omv 6690 oa0 6692 om0 6693 oei0 6694 omcl 6696 omv2 6700 oaword1 6706 nna0r 6713 nnm0r 6714 card0 7486 |
| Copyright terms: Public domain | W3C validator |