Theorem 1n0 8414

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 8403	. 2 ⊢ 1o = {∅}
2		0ex 5242	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4721	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3003	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2933  ∅c0 4274  {csn 4568  1_oc1o 8389

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-un 3895  df-nul 4275  df-sn 4569  df-suc 6321  df-1o 8396

This theorem is referenced by:  nlim1  8415  xp01disj  8417  xp01disjl  8418  enpr2d  8986  map2xp  9076  snnen2o  9146  0sdom1dom  9147  sdom1  9151  rex2dom  9154  1sdom2dom  9155  unxpdom2  9161  sucxpdom  9162  ssttrcl  9625  ttrclselem2  9636  djuin  9831  eldju2ndl  9837  updjudhcoinrg  9846  card1  9881  pm54.43lem  9913  cflim2  10174  isfin4p1  10226  dcomex  10358  pwcfsdom  10495  cfpwsdom  10496  canthp1lem2  10565  wunex2  10650  1pi  10795  fnpr2o  17510  fnpr2ob  17511  fvpr0o  17512  fvpr1o  17513  fvprif  17514  xpsfrnel  17515  setcepi  18044  setc2obas  18050  frgpuptinv  19735  frgpup3lem  19741  frgpnabllem1  19837  dmdprdpr  20015  dprdpr  20016  coe1mul2lem1  22241  2ndcdisj  23430  xpstopnlem1  23783  ltsval2  27639  nosgnn0  27641  ltsintdifex  27644  ltsres  27645  nogesgn1ores  27657  ltssolem1  27658  nosepnelem  27662  nogt01o  27679  noinfbnd1lem3  27708  noinfbnd2lem1  27713  bnj906  35093  gonan0  35595  gonar  35598  fmla0disjsuc  35601  rankeq1o  36374  onint1  36652  bj-disjsn01  37272  bj-0nel1  37273  bj-1nel0  37274  bj-pr21val  37333  bj-pr22val  37339  finxp1o  37719  finxp2o  37726  domalom  37731  wepwsolem  43485  onov0suclim  43717  clsk3nimkb  44482  clsk1indlem4  44486  clsk1indlem1  44487  nelsubc3  49543  prsthinc  49936  prstchom  50034  prstchom2ALT  50036