![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 0elon | Structured version Visualization version GIF 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 | ⊢ ∅ ∈ On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ord0 6367 | . 2 ⊢ Ord ∅ | |
2 | 0ex 5263 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | elon 6323 | . 2 ⊢ (∅ ∈ On ↔ Ord ∅) |
4 | 1, 3 | mpbir 230 | 1 ⊢ ∅ ∈ On |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ∅c0 4281 Ord word 6313 Oncon0 6314 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2709 ax-nul 5262 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2943 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-tr 5222 df-po 5543 df-so 5544 df-fr 5586 df-we 5588 df-ord 6317 df-on 6318 |
This theorem is referenced by: inton 6372 onn0 6379 on0eqel 6437 orduninsuc 7770 onzsl 7773 peano1 7816 smofvon2 8270 tfrlem16 8307 rdg0n 8348 1on 8392 1onOLD 8393 ordgt0ge1 8407 oa0 8430 om0 8431 oe0m 8432 oe0m0 8434 oe0 8436 oesuclem 8439 omcl 8450 oecl 8451 oa0r 8452 om0r 8453 oaord1 8466 oaword1 8467 oaword2 8468 oawordeu 8470 oa00 8474 odi 8494 oeoa 8512 oeoe 8514 nna0r 8524 nnm0r 8525 card2on 9424 card2inf 9425 harcl 9429 cantnfvalf 9535 rankon 9665 cardon 9814 card0 9828 alephon 9939 alephgeom 9952 alephfplem1 9974 djufi 10056 ttukeylem4 10382 ttukeylem7 10385 cfpwsdom 10454 inar1 10645 rankcf 10647 gruina 10688 sltval2 26932 sltsolem1 26951 nosepnelem 26955 nodense 26968 nolt02o 26971 bdayelon 27044 old0 27117 made0 27131 bnj168 33122 rdgprc0 34162 naddid1 34232 naddword1 34239 rankeq1o 34687 0hf 34693 onsucconn 34841 onsucsuccmp 34847 finxp1o 35794 finxpreclem4 35796 harn0 41331 omabs2 41459 omcl3g 41461 naddcnff 41470 safesnsupfiss 41486 safesnsupfidom1o 41488 safesnsupfilb 41489 0no 41506 nlim1NEW 41513 aleph1min 41628 |
Copyright terms: Public domain | W3C validator |