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 6388 | . 2 | |
2 | c0 3414 | . . 3 | |
3 | 2 | csuc 4350 | . 2 |
4 | 1, 3 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 1on 6402 df1o2 6408 ordgt0ge1 6414 oa1suc 6446 1onn 6499 nnm1 6504 nlt1pig 7303 indpi 7304 1tonninf 10396 hash1 10746 012of 14028 2o01f 14029 pwle2 14031 isomninnlem 14062 iswomninnlem 14081 ismkvnnlem 14084 |
Copyright terms: Public domain | W3C validator |