HomeRelated theorems
GIF version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Define the ordinal number 1. |
| Ref | Expression |
|---|---|
| df-1o | ⊢ 1o = suc ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | c1o 4118 | . 2 class 1o | |
| 2 | c0 2276 | . . 3 class ∅ | |
| 3 | 2 | csuc 2945 | . 2 class suc ∅ |
| 4 | 1, 3 | wceq 954 | 1 wff 1o = suc ∅ |
| Colors of variables: wff set class |
| This definition is referenced by: 1on 4128 df1o2 4130 ordgt0ge1 4134 oa1suc 4154 om1 4166 oe1 4168 oelim2 4212 nnecl 4221 1onn 4243 0sdom1dom 4510 aleph1 4851 nlt1pi 5013 indpi 5014 aleph1re 7502 |