![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > on0eln0 | Structured version Visualization version Unicode version |
Description: An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004.) |
Ref | Expression |
---|---|
on0eln0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eloni 5433 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ord0eln0 5477 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pr 4639 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-sbc 3268 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-br 4403 df-opab 4462 df-tr 4498 df-eprel 4745 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-ord 5426 df-on 5427 |
This theorem is referenced by: ondif1 7203 oe0lem 7215 oevn0 7217 oa00 7260 omord 7269 om00 7276 om00el 7277 omeulem1 7283 omeulem2 7284 oewordri 7293 oeordsuc 7295 oelim2 7296 oeoa 7298 oeoe 7300 oeeui 7303 omabs 7348 omxpenlem 7673 cantnff 8179 cantnfp1lem2 8184 cantnfp1lem3 8185 cantnfp1 8186 cantnflem1d 8193 cantnflem1 8194 cantnflem3 8196 cantnflem4 8197 cantnf 8198 cnfcomlem 8204 cnfcom3 8209 r1tskina 9207 onsucconi 31097 onint1 31109 frlmpwfi 35956 |
Copyright terms: Public domain | W3C validator |