![]() |
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 6410 |
. 2
![]() ![]() | |
2 | c1o 6409 |
. . 3
![]() ![]() | |
3 | 2 | csuc 4365 |
. 2
![]() ![]() ![]() |
4 | 1, 3 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 2on 6425 2on0 6426 df2o3 6430 o1p1e2 6468 2onn 6521 nnm2 6526 enpr2d 6816 snnen2og 6858 1nen2 6860 pm54.43 7188 en2eleq 7193 en2other2 7194 exmidfodomrlemr 7200 exmidfodomrlemrALT 7201 prarloclemarch2 7417 prarloclemlt 7491 prarloclemn 7497 hash2 10791 bj-el2oss1o 14496 pwle2 14718 nnsf 14724 |
Copyright terms: Public domain | W3C validator |