Theorem 1n0 8451

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 8432	. 2 ⊢ 1o = suc ∅
2		nsuceq0 6427	. 2 ⊢ suc ∅ ≠ ∅
3	1, 2	eqnetri 3026	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2956  ∅c0 4285  suc csuc 6344  1_oc1o 8425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3455  df-dif 3907  df-un 3909  df-nul 4286  df-sn 4582  df-suc 6348  df-1o 8432

This theorem is referenced by:  nlim1  8453  xp01disj  8455  xp01disjl  8456  enpr2d  9025  map2xp  9115  snnen2o  9185  0sdom1dom  9186  sdom1  9190  rex2dom  9193  1sdom2dom  9194  unxpdom2  9200  sucxpdom  9201  ssttrcl  9667  ttrclselem2  9678  djuin  9873  eldju2ndl  9879  updjudhcoinrg  9888  card1  9923  pm54.43lem  9955  cflim2  10217  isfin4p1  10269  dcomex  10401  pwcfsdom  10538  cfpwsdom  10539  canthp1lem2  10608  wunex2  10693  1pi  10838  fnpr2o  17570  fnpr2ob  17571  fvpr0o  17572  fvpr1o  17573  fvprif  17574  xpsfrnel  17575  setcepi  18104  setc2obas  18110  frgpuptinv  19794  frgpup3lem  19800  frgpnabllem1  19896  dmdprdpr  20074  dprdpr  20075  coe1mul2lem1  22310  2ndcdisj  23496  xpstopnlem1  23849  ltsval2  27697  nosgnn0  27699  ltsintdifex  27702  ltsres  27703  nogesgn1ores  27715  ltssolem1  27716  nosepnelem  27720  nogt01o  27737  noinfbnd1lem3  27766  noinfbnd2lem1  27771  bnj906  35189  gonan0  35706  gonar  35709  fmla0disjsuc  35712  rankeq1o  36485  onint1  36773  bj-disjsn01  37401  bj-0nel1  37402  bj-1nel0  37403  bj-pr21val  37462  bj-pr22val  37468  finxp1o  37850  finxp2o  37857  domalom  37862  wepwsolem  43583  onov0suclim  43815  clsk3nimkb  44580  clsk1indlem4  44584  clsk1indlem1  44585  nelsubc3  49656  prsthinc  50049  prstchom  50147  prstchom2ALT  50149