| 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 6486 | . 2 class 2o | |
| 2 | c1o 6485 | . . 3 class 1o | |
| 3 | 2 | csuc 4410 | . 2 class suc 1o |
| 4 | 1, 3 | wceq 1372 | 1 wff 2o = suc 1o |
| Colors of variables: wff set class |
| This definition is referenced by: 2on 6501 2on0 6502 df2o3 6506 o1p1e2 6544 2onn 6597 nnm2 6602 enpr2d 6894 snnen2og 6938 1nen2 6940 pm54.43 7280 en2eleq 7285 en2other2 7286 exmidfodomrlemr 7292 exmidfodomrlemrALT 7293 prarloclemarch2 7514 prarloclemlt 7588 prarloclemn 7594 hash2 10938 bj-el2oss1o 15574 pwle2 15799 nnsf 15806 |
| Copyright terms: Public domain | W3C validator |