Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-1o | GIF version |
Description: Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
Ref | Expression |
---|---|
df-1o | ⊢ 1o = suc ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c1o 6368 | . 2 class 1o | |
2 | c0 3404 | . . 3 class ∅ | |
3 | 2 | csuc 4337 | . 2 class suc ∅ |
4 | 1, 3 | wceq 1342 | 1 wff 1o = suc ∅ |
Colors of variables: wff set class |
This definition is referenced by: 1on 6382 df1o2 6388 ordgt0ge1 6394 oa1suc 6426 1onn 6479 nnm1 6483 nlt1pig 7273 indpi 7274 1tonninf 10365 hash1 10713 012of 13716 2o01f 13717 pwle2 13719 isomninnlem 13750 iswomninnlem 13769 ismkvnnlem 13772 |
Copyright terms: Public domain | W3C validator |