Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-1o | Unicode version |
Description: Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
Ref | Expression |
---|---|
df-1o |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c1o 6358 | . 2 | |
2 | c0 3395 | . . 3 | |
3 | 2 | csuc 4327 | . 2 |
4 | 1, 3 | wceq 1335 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 1on 6372 df1o2 6378 ordgt0ge1 6384 oa1suc 6416 1onn 6469 nnm1 6473 nlt1pig 7263 indpi 7264 1tonninf 10348 hash1 10696 012of 13638 2o01f 13639 pwle2 13641 isomninnlem 13672 iswomninnlem 13691 ismkvnnlem 13694 |
Copyright terms: Public domain | W3C validator |