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 8086 | . 2 class 1o | |
2 | c0 4290 | . . 3 class ∅ | |
3 | 2 | csuc 6187 | . 2 class suc ∅ |
4 | 1, 3 | wceq 1528 | 1 wff 1o = suc ∅ |
Colors of variables: wff setvar class |
This definition is referenced by: 1on 8100 df1o2 8107 ordgt0ge1 8113 oa1suc 8147 om1 8158 oe1 8160 oelim2 8211 nnecl 8229 1onn 8255 omabs 8264 nnm1 8265 0sdom1dom 8705 ackbij1lem14 9644 aleph1 9982 cfpwsdom 9995 nlt1pi 10317 indpi 10318 hash1 13755 aleph1re 15588 bnj168 31900 satfv1 32508 fmla1 32532 sltval2 33061 sltsolem1 33078 nosepnelem 33082 nolt02o 33097 rankeq1o 33530 finxp1o 34556 finxpreclem4 34558 finxp00 34566 aleph1min 39796 clsk1indlem1 40275 |
Copyright terms: Public domain | W3C validator |