| 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. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 17-Sep-1993.) |
| Ref | Expression |
|---|---|
| 0elon | ⊢ ∅ ∈ On |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ord0 6437 | . 2 ⊢ Ord ∅ | |
| 2 | 0ex 5307 | . . 3 ⊢ ∅ ∈ V | |
| 3 | 2 | elon 6393 | . 2 ⊢ (∅ ∈ On ↔ Ord ∅) |
| 4 | 1, 3 | mpbir 231 | 1 ⊢ ∅ ∈ On |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 ∅c0 4333 Ord word 6383 Oncon0 6384 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-nul 5306 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-tr 5260 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-ord 6387 df-on 6388 |
| This theorem is referenced by: inton 6442 onn0 6449 on0eqel 6508 orduninsuc 7864 onzsl 7867 peano1 7910 smofvon2 8396 tfrlem16 8433 rdg0n 8474 1on 8518 1onOLD 8519 ordgt0ge1 8531 oa0 8554 om0 8555 oe0m 8556 oe0m0 8558 oe0 8560 oesuclem 8563 omcl 8574 oecl 8575 oa0r 8576 om0r 8577 oaord1 8589 oaword1 8590 oaword2 8591 oawordeu 8593 oa00 8597 odi 8617 oeoa 8635 oeoe 8637 nna0r 8647 nnm0r 8648 naddrid 8721 naddlid 8722 naddword1 8729 card2on 9594 card2inf 9595 harcl 9599 cantnfvalf 9705 rankon 9835 cardon 9984 card0 9998 alephon 10109 alephgeom 10122 alephfplem1 10144 djufi 10227 ttukeylem4 10552 ttukeylem7 10555 cfpwsdom 10624 inar1 10815 rankcf 10817 gruina 10858 sltval2 27701 sltsolem1 27720 nosepnelem 27724 nodense 27737 nolt02o 27740 bdayelon 27821 cuteq1 27878 old0 27898 made0 27912 old1 27914 mulsproplem2 28143 mulsproplem3 28144 mulsproplem4 28145 mulsproplem5 28146 mulsproplem6 28147 mulsproplem7 28148 mulsproplem8 28149 mulsproplem12 28153 mulsproplem13 28154 mulsproplem14 28155 precsexlem1 28231 precsexlem2 28232 bnj168 34744 rdgprc0 35794 rankeq1o 36172 0hf 36178 onsucconn 36439 onsucsuccmp 36445 finxp1o 37393 finxpreclem4 37395 harn0 43114 onexoegt 43256 ordeldif1o 43273 oe0suclim 43290 oaordnr 43309 nnoeomeqom 43325 oenass 43332 omabs2 43345 omcl3g 43347 naddcnff 43375 nadd2rabex 43399 safesnsupfiss 43428 safesnsupfidom1o 43430 safesnsupfilb 43431 0no 43448 nlim1NEW 43455 aleph1min 43570 wfaxrep 45011 wfaxnul 45013 |
| Copyright terms: Public domain | W3C validator |