Theorem 1n0 8473

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 8454	. 2 ⊢ 1o = suc ∅
2		nsuceq0 6448	. 2 ⊢ suc ∅ ≠ ∅
3	1, 2	eqnetri 3028	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2958  ∅c0 4287  suc csuc 6364  1_oc1o 8447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457  df-dif 3909  df-un 3911  df-nul 4288  df-sn 4591  df-suc 6368  df-1o 8454

This theorem is referenced by:  nlim1  8475  xp01disj  8477  xp01disjl  8478  enpr2d  9046  map2xp  9136  snnen2o  9206  0sdom1dom  9207  sdom1  9211  rex2dom  9214  1sdom2dom  9215  unxpdom2  9221  sucxpdom  9222  ssttrcl  9685  ttrclselem2  9696  djuin  9905  eldju2ndl  9911  updjudhcoinrg  9920  card1  9955  pm54.43lem  9987  cflim2  10248  isfin4p1  10300  dcomex  10432  pwcfsdom  10569  cfpwsdom  10570  canthp1lem2  10639  wunex2  10724  1pi  10869  fnpr2o  17612  fnpr2ob  17613  fvpr0o  17614  fvpr1o  17615  fvprif  17616  xpsfrnel  17617  setcepi  18146  setc2obas  18152  frgpuptinv  19842  frgpup3lem  19848  frgpnabllem1  19944  dmdprdpr  20122  dprdpr  20123  coe1mul2lem1  22409  2ndcdisj  23594  xpstopnlem1  23947  ltsval2  27798  nosgnn0  27800  ltsintdifex  27803  ltsres  27804  nogesgn1ores  27816  ltssolem1  27817  nosepnelem  27821  nogt01o  27838  noinfbnd1lem3  27867  noinfbnd2lem1  27872  bnj906  35296  gonan0  35862  gonar  35865  fmla0disjsuc  35868  rankeq1o  36641  onint1  36938  bj-disjsn01  37566  bj-0nel1  37567  bj-1nel0  37568  bj-pr21val  37627  bj-pr22val  37633  finxp1o  38016  finxp2o  38023  domalom  38028  wepwsolem  43749  onov0suclim  43981  clsk3nimkb  44746  clsk1indlem4  44750  clsk1indlem1  44751  nelsubc3  49826  prsthinc  50219  prstchom  50317  prstchom2ALT  50319