![]() |
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 6314 |
. 2
![]() ![]() | |
2 | c0 3368 |
. . 3
![]() ![]() | |
3 | 2 | csuc 4295 |
. 2
![]() ![]() ![]() |
4 | 1, 3 | wceq 1332 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 1on 6328 df1o2 6334 ordgt0ge1 6340 oa1suc 6371 1onn 6424 nnm1 6428 nlt1pig 7173 indpi 7174 1tonninf 10244 hash1 10589 012of 13363 2o01f 13364 pwle2 13366 isomninnlem 13400 iswomninnlem 13417 ismkvnnlem 13419 |
Copyright terms: Public domain | W3C validator |