Theorem 1n0 8425

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

Syntax hints:   ≠ wne 2933  ∅c0 4287  {csn 4582  1_oc1o 8400

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 5253

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 3444  df-dif 3906  df-un 3908  df-nul 4288  df-sn 4583  df-suc 6331  df-1o 8407

This theorem is referenced by:  nlim1  8426  xp01disj  8428  xp01disjl  8429  enpr2d  8997  map2xp  9087  snnen2o  9157  0sdom1dom  9158  sdom1  9162  rex2dom  9165  1sdom2dom  9166  unxpdom2  9172  sucxpdom  9173  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  17490  fnpr2ob  17491  fvpr0o  17492  fvpr1o  17493  fvprif  17494  xpsfrnel  17495  setcepi  18024  setc2obas  18030  frgpuptinv  19712  frgpup3lem  19718  frgpnabllem1  19814  dmdprdpr  19992  dprdpr  19993  coe1mul2lem1  22221  2ndcdisj  23412  xpstopnlem1  23765  ltsval2  27636  nosgnn0  27638  ltsintdifex  27641  ltsres  27642  nogesgn1ores  27654  ltssolem1  27655  nosepnelem  27659  nogt01o  27676  noinfbnd1lem3  27705  noinfbnd2lem1  27710  bnj906  35105  gonan0  35605  gonar  35608  fmla0disjsuc  35611  rankeq1o  36384  onint1  36662  bj-disjsn01  37197  bj-0nel1  37198  bj-1nel0  37199  bj-pr21val  37258  bj-pr22val  37264  finxp1o  37644  finxp2o  37651  domalom  37656  wepwsolem  43396  onov0suclim  43628  clsk3nimkb  44393  clsk1indlem4  44397  clsk1indlem1  44398  nelsubc3  49427  prsthinc  49820  prstchom  49918  prstchom2ALT  49920