Theorem 1n0 8423

Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)

Assertion

Ref	Expression
1n0	⊢ 1o ≠ ∅

Proof of Theorem 1n0

Step	Hyp	Ref	Expression
1		df1o2 8412	. 2 ⊢ 1o = {∅}
2		0ex 5242	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4720	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3002	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2932  ∅c0 4273  {csn 4567  1_oc1o 8398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-un 3894  df-nul 4274  df-sn 4568  df-suc 6329  df-1o 8405

This theorem is referenced by:  nlim1  8424  xp01disj  8426  xp01disjl  8427  enpr2d  8995  map2xp  9085  snnen2o  9155  0sdom1dom  9156  sdom1  9160  rex2dom  9163  1sdom2dom  9164  unxpdom2  9170  sucxpdom  9171  ssttrcl  9636  ttrclselem2  9647  djuin  9842  eldju2ndl  9848  updjudhcoinrg  9857  card1  9892  pm54.43lem  9924  cflim2  10185  isfin4p1  10237  dcomex  10369  pwcfsdom  10506  cfpwsdom  10507  canthp1lem2  10576  wunex2  10661  1pi  10806  fnpr2o  17521  fnpr2ob  17522  fvpr0o  17523  fvpr1o  17524  fvprif  17525  xpsfrnel  17526  setcepi  18055  setc2obas  18061  frgpuptinv  19746  frgpup3lem  19752  frgpnabllem1  19848  dmdprdpr  20026  dprdpr  20027  coe1mul2lem1  22232  2ndcdisj  23421  xpstopnlem1  23774  ltsval2  27620  nosgnn0  27622  ltsintdifex  27625  ltsres  27626  nogesgn1ores  27638  ltssolem1  27639  nosepnelem  27643  nogt01o  27660  noinfbnd1lem3  27689  noinfbnd2lem1  27694  bnj906  35072  gonan0  35574  gonar  35577  fmla0disjsuc  35580  rankeq1o  36353  onint1  36631  bj-disjsn01  37259  bj-0nel1  37260  bj-1nel0  37261  bj-pr21val  37320  bj-pr22val  37326  finxp1o  37708  finxp2o  37715  domalom  37720  wepwsolem  43470  onov0suclim  43702  clsk3nimkb  44467  clsk1indlem4  44471  clsk1indlem1  44472  nelsubc3  49546  prsthinc  49939  prstchom  50037  prstchom2ALT  50039