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 8110 | . 2 ⊢ 1o = {∅} | |
2 | 0ex 5204 | . . 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 4291 {csn 4561 1oc1o 8089 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-nul 5203 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-v 3497 df-dif 3939 df-un 3941 df-nul 4292 df-sn 4562 df-suc 6192 df-1o 8096 |
This theorem is referenced by: xp01disj 8114 xp01disjl 8115 map2xp 8681 sdom1 8712 1sdom 8715 unxpdom2 8720 sucxpdom 8721 djuin 9341 eldju2ndl 9347 updjudhcoinrg 9356 card1 9391 pm54.43lem 9422 cflim2 9679 isfin4p1 9731 dcomex 9863 pwcfsdom 9999 cfpwsdom 10000 canthp1lem2 10069 wunex2 10154 1pi 10299 fnpr2o 16824 fnpr2ob 16825 fvpr0o 16826 fvpr1o 16827 fvprif 16828 xpsfrnel 16829 setcepi 17342 frgpuptinv 18891 frgpup3lem 18897 frgpnabllem1 18987 dmdprdpr 19165 dprdpr 19166 coe1mul2lem1 20429 2ndcdisj 22058 xpstopnlem1 22411 bnj906 32197 gonan0 32634 gonar 32637 fmla0disjsuc 32640 sltval2 33158 nosgnn0 33160 sltintdifex 33163 sltres 33164 sltsolem1 33175 nosepnelem 33179 rankeq1o 33627 onint1 33792 bj-disjsn01 34259 bj-0nel1 34260 bj-1nel0 34261 bj-pr21val 34320 bj-pr22val 34326 finxp1o 34667 finxp2o 34674 domalom 34679 wepwsolem 39635 clsk3nimkb 40383 clsk1indlem4 40387 clsk1indlem1 40388 |
Copyright terms: Public domain | W3C validator |