| 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 8513 | . 2 ⊢ 1o = {∅} | |
| 2 | 0ex 5307 | . . 3 ⊢ ∅ ∈ V | |
| 3 | 2 | snnz 4776 | . 2 ⊢ {∅} ≠ ∅ |
| 4 | 1, 3 | eqnetri 3011 | 1 ⊢ 1o ≠ ∅ |
| Colors of variables: wff setvar class |
| Syntax hints: ≠ wne 2940 ∅c0 4333 {csn 4626 1oc1o 8499 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-nul 5306 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-v 3482 df-dif 3954 df-un 3956 df-nul 4334 df-sn 4627 df-suc 6390 df-1o 8506 |
| This theorem is referenced by: nlim1 8527 xp01disj 8529 xp01disjl 8530 enpr2d 9089 map2xp 9187 snnen2o 9273 0sdom1dom 9274 sdom1 9278 sdom1OLD 9279 rex2dom 9282 1sdom2dom 9283 1sdomOLD 9285 unxpdom2 9290 sucxpdom 9291 ssttrcl 9755 ttrclselem2 9766 djuin 9958 eldju2ndl 9964 updjudhcoinrg 9973 card1 10008 pm54.43lem 10040 cflim2 10303 isfin4p1 10355 dcomex 10487 pwcfsdom 10623 cfpwsdom 10624 canthp1lem2 10693 wunex2 10778 1pi 10923 fnpr2o 17602 fnpr2ob 17603 fvpr0o 17604 fvpr1o 17605 fvprif 17606 xpsfrnel 17607 setcepi 18133 setc2obas 18139 frgpuptinv 19789 frgpup3lem 19795 frgpnabllem1 19891 dmdprdpr 20069 dprdpr 20070 coe1mul2lem1 22270 2ndcdisj 23464 xpstopnlem1 23817 sltval2 27701 nosgnn0 27703 sltintdifex 27706 sltres 27707 nogesgn1ores 27719 sltsolem1 27720 nosepnelem 27724 nogt01o 27741 noinfbnd1lem3 27770 noinfbnd2lem1 27775 bnj906 34944 gonan0 35397 gonar 35400 fmla0disjsuc 35403 rankeq1o 36172 onint1 36450 bj-disjsn01 36953 bj-0nel1 36954 bj-1nel0 36955 bj-pr21val 37014 bj-pr22val 37020 finxp1o 37393 finxp2o 37400 domalom 37405 wepwsolem 43054 onov0suclim 43287 clsk3nimkb 44053 clsk1indlem4 44057 clsk1indlem1 44058 prsthinc 49111 prstchom 49166 prstchom2ALT 49168 |
| Copyright terms: Public domain | W3C validator |