![]() |
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 6404 |
. 2
![]() ![]() | |
2 | c0 3422 |
. . 3
![]() ![]() | |
3 | 2 | csuc 4362 |
. 2
![]() ![]() ![]() |
4 | 1, 3 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 1on 6418 df1o2 6424 ordgt0ge1 6430 oa1suc 6462 1onn 6515 nnm1 6520 nlt1pig 7328 indpi 7329 1tonninf 10423 hash1 10772 012of 14394 2o01f 14395 pwle2 14397 isomninnlem 14427 iswomninnlem 14446 ismkvnnlem 14449 |
Copyright terms: Public domain | W3C validator |