![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1on | Unicode version |
Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) |
Ref | Expression |
---|---|
1on |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1o 6267 |
. 2
![]() ![]() ![]() ![]() ![]() | |
2 | 0elon 4274 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | onsuci 4392 |
. 2
![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | eqeltri 2187 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-13 1474 ax-14 1475 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-sep 4006 ax-nul 4014 ax-pow 4058 ax-pr 4091 ax-un 4315 |
This theorem depends on definitions: df-bi 116 df-tru 1317 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ral 2395 df-rex 2396 df-v 2659 df-dif 3039 df-un 3041 df-in 3043 df-ss 3050 df-nul 3330 df-pw 3478 df-sn 3499 df-pr 3500 df-uni 3703 df-tr 3987 df-iord 4248 df-on 4250 df-suc 4253 df-1o 6267 |
This theorem is referenced by: 1oex 6275 2on 6276 2on0 6277 2oconcl 6290 fnoei 6302 oeiexg 6303 oeiv 6306 oei0 6309 oeicl 6312 o1p1e2 6318 oawordriexmid 6320 endisj 6671 snexxph 6790 djuex 6880 1stinr 6913 2ndinr 6914 pm54.43 6996 xpdjuen 7022 prarloclemarch2 7175 nnsf 12891 |
Copyright terms: Public domain | W3C validator |