| 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 6495 | . 2 class 2o | |
| 2 | c1o 6494 | . . 3 class 1o | |
| 3 | 2 | csuc 4411 | . 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 6510 2on0 6511 df2o3 6515 o1p1e2 6553 2onn 6606 nnm2 6611 enpr2d 6910 snnen2og 6955 1nen2 6957 pm54.43 7297 en2eleq 7302 en2other2 7303 exmidfodomrlemr 7309 exmidfodomrlemrALT 7310 prarloclemarch2 7531 prarloclemlt 7605 prarloclemn 7611 hash2 10955 bj-el2oss1o 15643 pwle2 15868 nnsf 15875 |
| Copyright terms: Public domain | W3C validator |