![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-2o | GIF version |
Description: Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
Ref | Expression |
---|---|
df-2o | ⊢ 2o = suc 1o |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c2o 6404 | . 2 class 2o | |
2 | c1o 6403 | . . 3 class 1o | |
3 | 2 | csuc 4361 | . 2 class suc 1o |
4 | 1, 3 | wceq 1353 | 1 wff 2o = suc 1o |
Colors of variables: wff set class |
This definition is referenced by: 2on 6419 2on0 6420 df2o3 6424 o1p1e2 6462 2onn 6515 nnm2 6520 enpr2d 6810 snnen2og 6852 1nen2 6854 pm54.43 7182 en2eleq 7187 en2other2 7188 exmidfodomrlemr 7194 exmidfodomrlemrALT 7195 prarloclemarch2 7396 prarloclemlt 7470 prarloclemn 7476 hash2 10763 bj-el2oss1o 14148 pwle2 14370 nnsf 14377 |
Copyright terms: Public domain | W3C validator |