![]() |
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 6411 |
. 2
![]() ![]() | |
2 | c1o 6410 |
. . 3
![]() ![]() | |
3 | 2 | csuc 4366 |
. 2
![]() ![]() ![]() |
4 | 1, 3 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 2on 6426 2on0 6427 df2o3 6431 o1p1e2 6469 2onn 6522 nnm2 6527 enpr2d 6817 snnen2og 6859 1nen2 6861 pm54.43 7189 en2eleq 7194 en2other2 7195 exmidfodomrlemr 7201 exmidfodomrlemrALT 7202 prarloclemarch2 7418 prarloclemlt 7492 prarloclemn 7498 hash2 10792 bj-el2oss1o 14529 pwle2 14751 nnsf 14757 |
Copyright terms: Public domain | W3C validator |