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 7440 | . 2 class 1𝑜 | |
2 | c0 3874 | . . 3 class ∅ | |
3 | 2 | csuc 5642 | . 2 class suc ∅ |
4 | 1, 3 | wceq 1475 | 1 wff 1𝑜 = suc ∅ |
Colors of variables: wff setvar class |
This definition is referenced by: 1on 7454 df1o2 7459 ordgt0ge1 7464 oa1suc 7498 om1 7509 oe1 7511 oelim2 7562 nnecl 7580 1onn 7606 omabs 7614 nnm1 7615 0sdom1dom 8043 ackbij1lem14 8938 aleph1 9272 cfpwsdom 9285 nlt1pi 9607 indpi 9608 hash1 13053 aleph1re 14813 bnj168 30052 sltval2 31053 sltsolem1 31067 rankeq1o 31448 bj-1ex 32131 finxp1o 32405 finxpreclem4 32407 finxp00 32415 clsk1indlem1 37363 |
Copyright terms: Public domain | W3C validator |