![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-1o | Structured version Unicode version |
Description: Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
Ref | Expression |
---|---|
df-1o |
![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c1o 7022 |
. 2
![]() ![]() | |
2 | c0 3744 |
. . 3
![]() ![]() | |
3 | 2 | csuc 4828 |
. 2
![]() ![]() ![]() |
4 | 1, 3 | wceq 1370 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: 1on 7036 df1o2 7041 ordgt0ge1 7046 oa1suc 7080 om1 7090 oe1 7092 oelim2 7143 nnecl 7161 1onn 7187 omabs 7195 nnm1 7196 0sdom1dom 7620 ackbij1lem14 8512 aleph1 8845 cfpwsdom 8858 nlt1pi 9185 indpi 9186 hash1 12279 aleph1re 13644 sltval2 27940 sltsolem1 27952 rankeq1o 28352 bnj168 32038 bj-1ex 32759 |
Copyright terms: Public domain | W3C validator |