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 8107 | . 2 ⊢ 1o = {∅} | |
2 | 0ex 5203 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | snnz 4705 | . 2 ⊢ {∅} ≠ ∅ |
4 | 1, 3 | eqnetri 3086 | 1 ⊢ 1o ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 3016 ∅c0 4290 {csn 4559 1oc1o 8086 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-nul 5202 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-v 3497 df-dif 3938 df-un 3940 df-nul 4291 df-sn 4560 df-suc 6191 df-1o 8093 |
This theorem is referenced by: xp01disj 8111 xp01disjl 8112 map2xp 8676 sdom1 8707 1sdom 8710 unxpdom2 8715 sucxpdom 8716 djuin 9336 eldju2ndl 9342 updjudhcoinrg 9351 card1 9386 pm54.43lem 9417 cflim2 9674 isfin4p1 9726 dcomex 9858 pwcfsdom 9994 cfpwsdom 9995 canthp1lem2 10064 wunex2 10149 1pi 10294 fnpr2o 16820 fnpr2ob 16821 fvpr0o 16822 fvpr1o 16823 fvprif 16824 xpsfrnel 16825 setcepi 17338 frgpuptinv 18828 frgpup3lem 18834 frgpnabllem1 18924 dmdprdpr 19102 dprdpr 19103 coe1mul2lem1 20365 2ndcdisj 21994 xpstopnlem1 22347 bnj906 32102 gonan0 32537 gonar 32540 fmla0disjsuc 32543 sltval2 33061 nosgnn0 33063 sltintdifex 33066 sltres 33067 sltsolem1 33078 nosepnelem 33082 rankeq1o 33530 onint1 33695 bj-disjsn01 34162 bj-0nel1 34163 bj-1nel0 34164 bj-pr21val 34223 bj-pr22val 34229 finxp1o 34556 finxp2o 34563 domalom 34568 wepwsolem 39522 clsk3nimkb 40270 clsk1indlem4 40274 clsk1indlem1 40275 |
Copyright terms: Public domain | W3C validator |