![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1n0 | Structured version Visualization version GIF version |
Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) |
Ref | Expression |
---|---|
1n0 | ⊢ 1o ≠ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df1o2 7967 | . 2 ⊢ 1o = {∅} | |
2 | 0ex 5102 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | snnz 4618 | . 2 ⊢ {∅} ≠ ∅ |
4 | 1, 3 | eqnetri 3054 | 1 ⊢ 1o ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 2984 ∅c0 4211 {csn 4472 1oc1o 7946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 ax-nul 5101 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-v 3439 df-dif 3862 df-un 3864 df-nul 4212 df-sn 4473 df-suc 6072 df-1o 7953 |
This theorem is referenced by: xp01disj 7971 xp01disjl 7972 map2xp 8534 sdom1 8564 1sdom 8567 unxpdom2 8572 sucxpdom 8573 djuin 9193 eldju2ndl 9199 updjudhcoinrg 9208 card1 9243 pm54.43lem 9274 cflim2 9531 isfin4p1 9583 dcomex 9715 pwcfsdom 9851 cfpwsdom 9852 canthp1lem2 9921 wunex2 10006 1pi 10151 fnpr2o 16659 fnpr2ob 16660 fvpr0o 16661 fvpr1o 16662 fvprif 16663 xpsfrnel 16664 setcepi 17177 frgpuptinv 18624 frgpup3lem 18630 frgpnabllem1 18716 dmdprdpr 18888 dprdpr 18889 coe1mul2lem1 20118 2ndcdisj 21748 xpstopnlem1 22101 bnj906 31818 gonan0 32248 gonar 32251 fmla0disjsuc 32254 sltval2 32773 nosgnn0 32775 sltintdifex 32778 sltres 32779 sltsolem1 32790 nosepnelem 32794 rankeq1o 33242 onint1 33407 bj-disjsn01 33839 bj-0nel1 33840 bj-1nel0 33841 bj-pr21val 33949 bj-pr22val 33955 finxp1o 34223 finxp2o 34230 domalom 34235 wepwsolem 39146 clsk3nimkb 39894 clsk1indlem4 39898 clsk1indlem1 39899 |
Copyright terms: Public domain | W3C validator |