Theorem 1n0 8479

Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

Ref	Expression
1n0	⊢ 1o ≠ ∅

Proof of Theorem 1n0

Step	Hyp	Ref	Expression
1		df-1o 8460	. 2 ⊢ 1o = suc ∅
2		nsuceq0 6441	. 2 ⊢ suc ∅ ≠ ∅
3	1, 2	eqnetri 3026	1 ⊢ 1o ≠ ∅

This proof depends on syntax axioms:   ≠ wne 2956  ∅c0 4279  suc csuc 6357  1_oc1o 8453

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-un 3904  df-nul 4280  df-sn 4585  df-suc 6361  df-1o 8460

This theorem is used by:  nlim1  8481  xp01disj  8483  xp01disjl  8484  enpr2d  9060  map2xp  9150  snnen2o  9220  0sdom1dom  9221  sdom1  9225  rex2dom  9228  1sdom2dom  9229  unxpdom2  9235  sucxpdom  9236  ssttrcl  9700  ttrclselem2  9711  djuin  9980  eldju2ndl  9986  updjudhcoinrg  9995  card1  10030  pm54.43lem  10062  cflim2  10322  isfin4p1  10374  dcomex  10506  pwcfsdom  10649  cfpwsdom  10650  canthp1lem2  10719  wunex2  10804  1pi  10949  fnpr2o  17709  fnpr2ob  17710  fvpr0o  17711  fvpr1o  17712  fvprif  17713  xpsfrnel  17714  setcepi  18243  setc2obas  18249  degenmgmnfn  19116  degenmgm  19117  degenmgm2  19120  frgpuptinv  19965  frgpup3lem  19971  frgpnabllem1  20067  dmdprdpr  20245  dprdpr  20246  coe1mul2lem1  22566  2ndcdisj  23755  xpstopnlem1  24108  ltsval2  27995  nosgnn0  27997  ltsintdifex  28000  ltsres  28001  nogesgn1ores  28013  ltssolem1  28014  nosepnelem  28018  nogt01o  28035  noinfbnd1lem3  28064  noinfbnd2lem1  28069  bnj906  35543  gonan0  36126  gonar  36129  fmla0disjsuc  36132  rankeq1o  36902  onint1  37207  bj-disjsn01  37835  bj-0nel1  37836  bj-1nel0  37837  bj-pr21val  37896  bj-pr22val  37902  finxp1o  38283  finxp2o  38290  domalom  38295  wepwsolem  44002  onov0suclim  44234  clsk3nimkb  44999  clsk1indlem4  45003  clsk1indlem1  45004  nelsubc3  50123  prsthinc  50516  prstchom  50614  prstchom2ALT  50616