![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > onss | Unicode version |
Description: An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.) |
Ref | Expression |
---|---|
onss |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eloni 4555 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ordsson 4733 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 16 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: onuni 4736 onminex 4750 suceloni 4756 onssi 4780 tfi 4796 tfr3 6623 tz7.49 6665 tz7.49c 6666 oacomf1olem 6770 oeeulem 6807 ordtypelem2 7448 cantnfcl 7582 cantnflt 7587 cantnfp1lem3 7596 oemapvali 7600 cantnflem1c 7603 cantnflem1d 7604 cantnflem1 7605 cantnf 7609 cnfcom 7617 cnfcom3lem 7620 infxpenlem 7855 ac10ct 7875 dfac12lem1 7983 dfac12lem2 7984 cfeq0 8096 cfsuc 8097 cff1 8098 cfflb 8099 cofsmo 8109 cfsmolem 8110 alephsing 8116 zorn2lem2 8337 ttukeylem3 8351 ttukeylem5 8353 ttukeylem6 8354 inar1 8610 predon 25411 soseq 25472 nobnddown 25573 nofulllem5 25578 ontgval 26089 aomclem6 27028 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2389 ax-sep 4294 ax-nul 4302 ax-pr 4367 ax-un 4664 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2262 df-mo 2263 df-clab 2395 df-cleq 2401 df-clel 2404 df-nfc 2533 df-ne 2573 df-ral 2675 df-rex 2676 df-rab 2679 df-v 2922 df-sbc 3126 df-dif 3287 df-un 3289 df-in 3291 df-ss 3298 df-pss 3300 df-nul 3593 df-if 3704 df-sn 3784 df-pr 3785 df-tp 3786 df-op 3787 df-uni 3980 df-br 4177 df-opab 4231 df-tr 4267 df-eprel 4458 df-po 4467 df-so 4468 df-fr 4505 df-we 4507 df-ord 4548 df-on 4549 |
Copyright terms: Public domain | W3C validator |