![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-1o | Structured version Visualization version GIF version |
Description: Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
Ref | Expression |
---|---|
df-1o | ⊢ 1o = suc ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c1o 7890 | . 2 class 1o | |
2 | c0 4173 | . . 3 class ∅ | |
3 | 2 | csuc 6025 | . 2 class suc ∅ |
4 | 1, 3 | wceq 1507 | 1 wff 1o = suc ∅ |
Colors of variables: wff setvar class |
This definition is referenced by: 1on 7904 df1o2 7910 ordgt0ge1 7916 oa1suc 7950 om1 7961 oe1 7963 oelim2 8014 nnecl 8032 1onn 8058 omabs 8066 nnm1 8067 0sdom1dom 8503 ackbij1lem14 9445 aleph1 9783 cfpwsdom 9796 nlt1pi 10118 indpi 10119 hash1 13569 aleph1re 15448 bnj168 31609 sltval2 32624 sltsolem1 32641 nosepnelem 32645 nolt02o 32660 rankeq1o 33093 finxp1o 34049 finxpreclem4 34051 finxp00 34059 clsk1indlem1 39703 |
Copyright terms: Public domain | W3C validator |