![]() |
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 | ⊢ 2𝑜 = suc 1𝑜 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c2o 5934 | . 2 class 2𝑜 | |
2 | c1o 5933 | . . 3 class 1𝑜 | |
3 | 2 | csuc 4068 | . 2 class suc 1𝑜 |
4 | 1, 3 | wceq 1242 | 1 wff 2𝑜 = suc 1𝑜 |
Colors of variables: wff set class |
This definition is referenced by: 2on 5948 2on0 5949 df2o3 5953 o1p1e2 5987 2onn 6030 nnm2 6034 prarloclemarch2 6402 prarloclemlt 6476 prarloclemn 6482 |
Copyright terms: Public domain | W3C validator |