![]() |
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 8480 | . 2 class 1o | |
2 | c0 4322 | . . 3 class ∅ | |
3 | 2 | csuc 6373 | . 2 class suc ∅ |
4 | 1, 3 | wceq 1533 | 1 wff 1o = suc ∅ |
Colors of variables: wff setvar class |
This definition is referenced by: df1o2 8494 1on 8499 1onOLD 8500 ordgt0ge1 8514 oa1suc 8552 o2p2e4 8562 om1 8563 oe1 8565 oelim2 8616 nnecl 8634 1onnALT 8662 omabs 8672 nnm1 8673 0sdom1domALT 9267 brttrcl2 9744 ssttrcl 9745 ttrcltr 9746 ttrclss 9750 dmttrcl 9751 rnttrcl 9752 ttrclselem2 9756 ackbij1lem14 10263 aleph1 10601 cfpwsdom 10614 nlt1pi 10936 indpi 10937 hash1 14404 aleph1re 16230 sltval2 27640 sltsolem1 27659 nosepnelem 27663 nolt02o 27679 bday1s 27815 cuteq1 27817 om2noseqlt 28227 bnj168 34494 satfv1 35106 fmla1 35130 rankeq1o 35900 finxp1o 37004 finxpreclem4 37006 finxp00 37014 ordeldif1o 42833 onov0suclim 42847 omabs2 42905 tfsconcatb0 42917 nlim1NEW 43016 aleph1min 43131 clsk1indlem1 43619 |
Copyright terms: Public domain | W3C validator |