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 6307 | . 2 | |
2 | c1o 6306 | . . 3 | |
3 | 2 | csuc 4287 | . 2 |
4 | 1, 3 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 2on 6322 2on0 6323 df2o3 6327 o1p1e2 6364 2onn 6417 nnm2 6421 enpr2d 6711 snnen2og 6753 1nen2 6755 infnninf 7022 nnnninf 7023 pm54.43 7046 en2eleq 7051 en2other2 7052 exmidfodomrlemr 7058 exmidfodomrlemrALT 7059 prarloclemarch2 7227 prarloclemlt 7301 prarloclemn 7307 hash2 10558 bj-el2oss1o 12981 pwle2 13193 nnsf 13199 |
Copyright terms: Public domain | W3C validator |