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 6369 | . 2 class 2o | |
2 | c1o 6368 | . . 3 class 1o | |
3 | 2 | csuc 4337 | . 2 class suc 1o |
4 | 1, 3 | wceq 1342 | 1 wff 2o = suc 1o |
Colors of variables: wff set class |
This definition is referenced by: 2on 6384 2on0 6385 df2o3 6389 o1p1e2 6427 2onn 6480 nnm2 6484 enpr2d 6774 snnen2og 6816 1nen2 6818 pm54.43 7137 en2eleq 7142 en2other2 7143 exmidfodomrlemr 7149 exmidfodomrlemrALT 7150 prarloclemarch2 7351 prarloclemlt 7425 prarloclemn 7431 hash2 10714 bj-el2oss1o 13496 pwle2 13719 nnsf 13726 |
Copyright terms: Public domain | W3C validator |