![]() |
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 6237 |
. 2
![]() ![]() | |
2 | c1o 6236 |
. . 3
![]() ![]() | |
3 | 2 | csuc 4225 |
. 2
![]() ![]() ![]() |
4 | 1, 3 | wceq 1299 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 2on 6252 2on0 6253 df2o3 6257 o1p1e2 6294 2onn 6347 nnm2 6351 snnen2og 6682 1nen2 6684 infnninf 6934 nnnninf 6935 pm54.43 6957 en2eleq 6960 en2other2 6961 exmidfodomrlemr 6967 exmidfodomrlemrALT 6968 prarloclemarch2 7128 prarloclemlt 7202 prarloclemn 7208 hash2 10399 pwle2 12779 nnsf 12783 |
Copyright terms: Public domain | W3C validator |