![]() |
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 | ⊢ 1𝑜 = suc ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c1o 7720 | . 2 class 1𝑜 | |
2 | c0 4056 | . . 3 class ∅ | |
3 | 2 | csuc 5884 | . 2 class suc ∅ |
4 | 1, 3 | wceq 1630 | 1 wff 1𝑜 = suc ∅ |
Colors of variables: wff setvar class |
This definition is referenced by: 1on 7734 df1o2 7739 ordgt0ge1 7744 oa1suc 7778 om1 7789 oe1 7791 oelim2 7842 nnecl 7860 1onn 7886 omabs 7894 nnm1 7895 0sdom1dom 8321 ackbij1lem14 9245 aleph1 9583 cfpwsdom 9596 nlt1pi 9918 indpi 9919 hash1 13382 aleph1re 15171 bnj168 31103 sltval2 32113 sltsolem1 32130 nosepnelem 32134 nolt02o 32149 rankeq1o 32582 bj-1ex 33242 finxp1o 33538 finxpreclem4 33540 finxp00 33548 clsk1indlem1 38843 |
Copyright terms: Public domain | W3C validator |