| 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. Definition 2.1 of [Schloeder] p. 4. (Contributed by NM, 29-Oct-1995.) |
| Ref | Expression |
|---|---|
| df-1o | ⊢ 1o = suc ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | c1o 8499 | . 2 class 1o | |
| 2 | c0 4333 | . . 3 class ∅ | |
| 3 | 2 | csuc 6386 | . 2 class suc ∅ |
| 4 | 1, 3 | wceq 1540 | 1 wff 1o = suc ∅ |
| Colors of variables: wff setvar class |
| This definition is referenced by: df1o2 8513 1on 8518 1onOLD 8519 ordgt0ge1 8531 oa1suc 8569 o2p2e4 8579 om1 8580 oe1 8582 oelim2 8633 nnecl 8651 1onnALT 8679 omabs 8689 nnm1 8690 0sdom1domALT 9275 brttrcl2 9754 ssttrcl 9755 ttrcltr 9756 ttrclss 9760 dmttrcl 9761 rnttrcl 9762 ttrclselem2 9766 ackbij1lem14 10272 aleph1 10611 cfpwsdom 10624 nlt1pi 10946 indpi 10947 hash1 14443 aleph1re 16281 sltval2 27701 sltsolem1 27720 nosepnelem 27724 nolt02o 27740 bday1s 27876 cuteq1 27878 om2noseqlt 28305 bnj168 34744 satfv1 35368 fmla1 35392 rankeq1o 36172 finxp1o 37393 finxpreclem4 37395 finxp00 37403 ordeldif1o 43273 onov0suclim 43287 omabs2 43345 tfsconcatb0 43357 nlim1NEW 43455 aleph1min 43570 clsk1indlem1 44058 |
| Copyright terms: Public domain | W3C validator |