![]() |
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 8469 | . 2 ⊢ 1o = {∅} | |
2 | 0ex 5298 | . . 3 ⊢ ∅ ∈ V | |
3 | 2 | snnz 4773 | . 2 ⊢ {∅} ≠ ∅ |
4 | 1, 3 | eqnetri 3003 | 1 ⊢ 1o ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 2932 ∅c0 4315 {csn 4621 1oc1o 8455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 ax-nul 5297 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-ne 2933 df-v 3468 df-dif 3944 df-un 3946 df-nul 4316 df-sn 4622 df-suc 6361 df-1o 8462 |
This theorem is referenced by: nlim1 8485 xp01disj 8487 xp01disjl 8488 enpr2d 9046 map2xp 9144 snnen2o 9234 0sdom1dom 9235 sdom1 9239 sdom1OLD 9240 rex2dom 9243 1sdom2dom 9244 1sdomOLD 9246 unxpdom2 9251 sucxpdom 9252 ssttrcl 9707 ttrclselem2 9718 djuin 9910 eldju2ndl 9916 updjudhcoinrg 9925 card1 9960 pm54.43lem 9992 cflim2 10255 isfin4p1 10307 dcomex 10439 pwcfsdom 10575 cfpwsdom 10576 canthp1lem2 10645 wunex2 10730 1pi 10875 fnpr2o 17504 fnpr2ob 17505 fvpr0o 17506 fvpr1o 17507 fvprif 17508 xpsfrnel 17509 setcepi 18042 setc2obas 18048 frgpuptinv 19683 frgpup3lem 19689 frgpnabllem1 19785 dmdprdpr 19963 dprdpr 19964 coe1mul2lem1 22110 2ndcdisj 23284 xpstopnlem1 23637 sltval2 27508 nosgnn0 27510 sltintdifex 27513 sltres 27514 nogesgn1ores 27526 sltsolem1 27527 nosepnelem 27531 nogt01o 27548 noinfbnd1lem3 27577 noinfbnd2lem1 27582 bnj906 34432 gonan0 34874 gonar 34877 fmla0disjsuc 34880 rankeq1o 35639 onint1 35825 bj-disjsn01 36324 bj-0nel1 36325 bj-1nel0 36326 bj-pr21val 36385 bj-pr22val 36391 finxp1o 36764 finxp2o 36771 domalom 36776 wepwsolem 42298 onov0suclim 42538 clsk3nimkb 43305 clsk1indlem4 43309 clsk1indlem1 43310 prsthinc 47886 prstchom 47909 prstchom2ALT 47911 |
Copyright terms: Public domain | W3C validator |