Theorem 1n0 8499

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

This proof depends on syntax axioms:   ≠ wne 2955  ∅c0 4278  suc csuc 6364  1_oc1o 8473

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 4047  df-un 4151  df-nul 4279  df-sn 4585  df-suc 6368  df-1o 8480

This theorem is used by:  nlim1  8501  xp01disj  8503  xp01disjl  8504  enpr2d  9080  map2xp  9170  snnen2o  9240  0sdom1dom  9241  sdom1  9245  rex2dom  9248  1sdom2dom  9249  unxpdom2  9255  sucxpdom  9256  ssttrcl  9720  ttrclselem2  9731  djuin  10003  eldju2ndl  10009  updjudhcoinrg  10018  card1  10053  pm54.43lem  10085  isfin4p1  10397  dcomex  10529  pwcfsdom  10672  cfpwsdom  10673  canthp1lem2  10742  wunex2  10827  1pi  10972  fnpr2o  17735  fnpr2ob  17736  fvpr0o  17737  fvpr1o  17738  fvprif  17739  xpsfrnel  17740  setcepi  18269  setc2obas  18275  degenmgmnfn  19142  degenmgm  19143  degenmgm2  19146  frgpuptinv  19991  frgpup3lem  19997  frgpnabllem1  20093  dmdprdpr  20271  dprdpr  20272  coe1mul2lem1  22592  2ndcdisj  23781  xpstopnlem1  24134  ltsval2  28019  nosgnn0  28021  ltsintdifex  28024  ltsres  28025  nogesgn1ores  28037  ltssolem1  28038  nosepnelem  28042  nogt01o  28059  noinfbnd1lem3  28088  noinfbnd2lem1  28093  bnj906  35607  gonan0  36244  gonar  36247  fmla0disjsuc  36250  rankeq1o  37025  onint1  37330  bj-disjsn01  37958  bj-0nel1  37959  bj-1nel0  37960  bj-pr21val  38019  bj-pr22val  38025  finxp1o  38409  finxp2o  38416  domalom  38421  wepwsolem  44143  onov0suclim  44370  clsk3nimkb  45134  clsk1indlem4  45138  clsk1indlem1  45139  nelsubc3  50279  prsthinc  50693  prstchom  50794  prstchom2ALT  50796  par2hom  50873  fuconuniqlem  50875