![]() |
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 6435 |
. 2
![]() ![]() | |
2 | c0 3437 |
. . 3
![]() ![]() | |
3 | 2 | csuc 4383 |
. 2
![]() ![]() ![]() |
4 | 1, 3 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 1on 6449 df1o2 6455 ordgt0ge1 6461 oa1suc 6493 1onn 6546 nnm1 6551 nlt1pig 7371 indpi 7372 1tonninf 10473 hash1 10826 012of 15224 2o01f 15225 pwle2 15227 isomninnlem 15257 iswomninnlem 15276 ismkvnnlem 15279 |
Copyright terms: Public domain | W3C validator |