![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1n0 | Structured version Visualization version Unicode version |
Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) |
Ref | Expression |
---|---|
1n0 |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df1o2 7191 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 0ex 4534 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | snnz 4089 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | eqnetri 2693 |
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 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-nul 4533 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-v 3046 df-dif 3406 df-un 3408 df-nul 3731 df-sn 3968 df-suc 5428 df-1o 7179 |
This theorem is referenced by: xp01disj 7195 map2xp 7739 sdom1 7769 1sdom 7772 unxpdom2 7777 sucxpdom 7778 card1 8399 pm54.43lem 8430 cflim2 8690 isfin4-3 8742 dcomex 8874 pwcfsdom 9005 cfpwsdom 9006 canthp1lem2 9075 wunex2 9160 1pi 9305 xpscfn 15458 xpsc0 15459 xpsc1 15460 xpscfv 15461 xpsfrnel 15462 xpsfrnel2 15464 setcepi 15976 frgpuptinv 17414 frgpup3lem 17420 frgpnabllem1 17502 dmdprdpr 17675 dprdpr 17676 coe1mul2lem1 18853 2ndcdisj 20464 xpstopnlem1 20817 bnj906 29734 sltval2 30536 nosgnn0 30538 sltintdifex 30543 sltres 30544 sltsolem1 30550 rankeq1o 30931 onint1 31102 bj-disjsn01 31536 bj-0nel1 31539 bj-1nel0 31540 bj-pr21val 31600 bj-pr22val 31606 finxp1o 31777 finxp2o 31784 wepwsolem 35894 |
Copyright terms: Public domain | W3C validator |