![]() |
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 | ⊢ 1𝑜 ≠ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df1o2 7729 | . 2 ⊢ 1𝑜 = {∅} | |
2 | 0ex 4925 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | snnz 4445 | . 2 ⊢ {∅} ≠ ∅ |
4 | 1, 3 | eqnetri 3013 | 1 ⊢ 1𝑜 ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 2943 ∅c0 4063 {csn 4317 1𝑜c1o 7709 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-nul 4924 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-v 3353 df-dif 3726 df-un 3728 df-nul 4064 df-sn 4318 df-suc 5871 df-1o 7716 |
This theorem is referenced by: xp01disj 7733 map2xp 8289 sdom1 8319 1sdom 8322 unxpdom2 8327 sucxpdom 8328 djuin 8947 eldju2ndl 8953 updjudhcoinrg 8962 card1 8997 pm54.43lem 9028 cflim2 9290 isfin4-3 9342 dcomex 9474 pwcfsdom 9610 cfpwsdom 9611 canthp1lem2 9680 wunex2 9765 1pi 9910 xpscfn 16426 xpsc0 16427 xpsc1 16428 xpscfv 16429 xpsfrnel 16430 xpsfrnel2 16432 setcepi 16944 frgpuptinv 18390 frgpup3lem 18396 frgpnabllem1 18482 dmdprdpr 18655 dprdpr 18656 coe1mul2lem1 19851 2ndcdisj 21479 xpstopnlem1 21832 bnj906 31337 sltval2 32145 nosgnn0 32147 sltintdifex 32150 sltres 32151 sltsolem1 32162 nosepnelem 32166 rankeq1o 32614 onint1 32784 bj-disjsn01 33268 bj-0nel1 33270 bj-1nel0 33271 bj-pr21val 33331 bj-pr22val 33337 finxp1o 33565 finxp2o 33572 wepwsolem 38138 clsk3nimkb 38864 clsk1indlem4 38868 clsk1indlem1 38869 |
Copyright terms: Public domain | W3C validator |