![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-2o | Unicode version |
Description: Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
Ref | Expression |
---|---|
df-2o |
![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c2o 6435 |
. 2
![]() ![]() | |
2 | c1o 6434 |
. . 3
![]() ![]() | |
3 | 2 | csuc 4383 |
. 2
![]() ![]() ![]() |
4 | 1, 3 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 2on 6450 2on0 6451 df2o3 6455 o1p1e2 6493 2onn 6546 nnm2 6551 enpr2d 6843 snnen2og 6887 1nen2 6889 pm54.43 7219 en2eleq 7224 en2other2 7225 exmidfodomrlemr 7231 exmidfodomrlemrALT 7232 prarloclemarch2 7448 prarloclemlt 7522 prarloclemn 7528 hash2 10824 bj-el2oss1o 14987 pwle2 15210 nnsf 15216 |
Copyright terms: Public domain | W3C validator |