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 6275 | . 2 class 2o | |
2 | c1o 6274 | . . 3 class 1o | |
3 | 2 | csuc 4257 | . 2 class suc 1o |
4 | 1, 3 | wceq 1316 | 1 wff 2o = suc 1o |
Colors of variables: wff set class |
This definition is referenced by: 2on 6290 2on0 6291 df2o3 6295 o1p1e2 6332 2onn 6385 nnm2 6389 enpr2d 6679 snnen2og 6721 1nen2 6723 infnninf 6990 nnnninf 6991 pm54.43 7014 en2eleq 7019 en2other2 7020 exmidfodomrlemr 7026 exmidfodomrlemrALT 7027 prarloclemarch2 7195 prarloclemlt 7269 prarloclemn 7275 hash2 10513 bj-el2oss1o 12877 pwle2 13089 nnsf 13095 |
Copyright terms: Public domain | W3C validator |