Theorem 1n0 8526

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 8507	. 2 ⊢ 1o = suc ∅
2		nsuceq0 6469	. 2 ⊢ suc ∅ ≠ ∅
3	1, 2	eqnetri 3029	1 ⊢ 1o ≠ ∅

This proof depends on syntax axioms:   ≠ wne 2959  ∅c0 4281  suc csuc 6385  1_oc1o 8500

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5264

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-suc 6389  df-1o 8507

This theorem is used by:  nlim1  8528  xp01disj  8530  xp01disjl  8531  enpr2d  9107  map2xp  9197  snnen2o  9267  0sdom1dom  9268  sdom1  9272  rex2dom  9275  1sdom2dom  9276  unxpdom2  9282  sucxpdom  9283  ssttrcl  9746  ttrclselem2  9757  djuin  10029  eldju2ndl  10035  updjudhcoinrg  10044  card1  10079  pm54.43lem  10111  isfin4p1  10423  dcomex  10555  pwcfsdom  10698  cfpwsdom  10699  canthp1lem2  10768  wunex2  10853  1pi  10998  fnpr2o  17761  fnpr2ob  17762  fvpr0o  17763  fvpr1o  17764  fvprif  17765  xpsfrnel  17766  setcepi  18295  setc2obas  18301  degenmgmnfn  19168  degenmgm  19169  degenmgm2  19172  frgpuptinv  20018  frgpup3lem  20024  frgpnabllem1  20120  dmdprdpr  20298  dprdpr  20299  coe1mul2lem1  22619  2ndcdisj  23808  xpstopnlem1  24161  ltsval2  28046  nosgnn0  28048  ltsintdifex  28051  ltsres  28052  nogesgn1ores  28064  ltssolem1  28065  nosepnelem  28069  nogt01o  28086  noinfbnd1lem3  28115  noinfbnd2lem1  28120  bnj906  35643  gonan0  36337  gonar  36340  fmla0disjsuc  36343  rankeq1o  37123  onint1  37428  bj-disjsn01  38056  bj-0nel1  38057  bj-1nel0  38058  bj-pr21val  38117  bj-pr22val  38123  finxp1o  38520  finxp2o  38527  domalom  38532  wepwsolem  44253  onov0suclim  44479  clsk3nimkb  45243  clsk1indlem4  45247  clsk1indlem1  45248  nelsubc3  50400  prsthinc  50814  prstchom  50915  prstchom2ALT  50917  par2hom  50994  fuconuniqlem  50996