Theorem 1n0 8481

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 8462	. 2 ⊢ 1o = suc ∅
2		nsuceq0 6453	. 2 ⊢ suc ∅ ≠ ∅
3	1, 2	eqnetri 3031	1 ⊢ 1o ≠ ∅

This proof depends on syntax axioms:   ≠ wne 2961  ∅c0 4289  suc csuc 6369  1_oc1o 8455

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 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-v 3460  df-dif 3911  df-un 3913  df-nul 4290  df-sn 4595  df-suc 6373  df-1o 8462

This theorem is used by:  nlim1  8483  xp01disj  8485  xp01disjl  8486  enpr2d  9055  map2xp  9145  snnen2o  9215  0sdom1dom  9216  sdom1  9220  rex2dom  9223  1sdom2dom  9224  unxpdom2  9230  sucxpdom  9231  ssttrcl  9694  ttrclselem2  9705  djuin  9923  eldju2ndl  9929  updjudhcoinrg  9938  card1  9973  pm54.43lem  10005  cflim2  10265  isfin4p1  10317  dcomex  10449  pwcfsdom  10586  cfpwsdom  10587  canthp1lem2  10656  wunex2  10741  1pi  10886  fnpr2o  17636  fnpr2ob  17637  fvpr0o  17638  fvpr1o  17639  fvprif  17640  xpsfrnel  17641  setcepi  18170  setc2obas  18176  frgpuptinv  19872  frgpup3lem  19878  frgpnabllem1  19974  dmdprdpr  20152  dprdpr  20153  coe1mul2lem1  22465  2ndcdisj  23650  xpstopnlem1  24003  ltsval2  27857  nosgnn0  27859  ltsintdifex  27862  ltsres  27863  nogesgn1ores  27875  ltssolem1  27876  nosepnelem  27880  nogt01o  27897  noinfbnd1lem3  27926  noinfbnd2lem1  27931  bnj906  35350  gonan0  35905  gonar  35908  fmla0disjsuc  35911  rankeq1o  36684  onint1  37001  bj-disjsn01  37629  bj-0nel1  37630  bj-1nel0  37631  bj-pr21val  37690  bj-pr22val  37696  finxp1o  38079  finxp2o  38086  domalom  38091  wepwsolem  43810  onov0suclim  44042  clsk3nimkb  44807  clsk1indlem4  44811  clsk1indlem1  44812  nelsubc3  49890  prsthinc  50283  prstchom  50381  prstchom2ALT  50383