Theorem 1n0 8498

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 8485	. 2 ⊢ 1o = {∅}
2		0ex 5277	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4752	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3002	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2932  ∅c0 4308  {csn 4601  1_oc1o 8471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-un 3931  df-nul 4309  df-sn 4602  df-suc 6358  df-1o 8478

This theorem is referenced by:  nlim1  8499  xp01disj  8501  xp01disjl  8502  enpr2d  9061  map2xp  9159  snnen2o  9243  0sdom1dom  9244  sdom1  9248  sdom1OLD  9249  rex2dom  9252  1sdom2dom  9253  1sdomOLD  9255  unxpdom2  9260  sucxpdom  9261  ssttrcl  9727  ttrclselem2  9738  djuin  9930  eldju2ndl  9936  updjudhcoinrg  9945  card1  9980  pm54.43lem  10012  cflim2  10275  isfin4p1  10327  dcomex  10459  pwcfsdom  10595  cfpwsdom  10596  canthp1lem2  10665  wunex2  10750  1pi  10895  fnpr2o  17569  fnpr2ob  17570  fvpr0o  17571  fvpr1o  17572  fvprif  17573  xpsfrnel  17574  setcepi  18099  setc2obas  18105  frgpuptinv  19750  frgpup3lem  19756  frgpnabllem1  19852  dmdprdpr  20030  dprdpr  20031  coe1mul2lem1  22202  2ndcdisj  23392  xpstopnlem1  23745  sltval2  27618  nosgnn0  27620  sltintdifex  27623  sltres  27624  nogesgn1ores  27636  sltsolem1  27637  nosepnelem  27641  nogt01o  27658  noinfbnd1lem3  27687  noinfbnd2lem1  27692  bnj906  34907  gonan0  35360  gonar  35363  fmla0disjsuc  35366  rankeq1o  36135  onint1  36413  bj-disjsn01  36916  bj-0nel1  36917  bj-1nel0  36918  bj-pr21val  36977  bj-pr22val  36983  finxp1o  37356  finxp2o  37363  domalom  37368  wepwsolem  43013  onov0suclim  43245  clsk3nimkb  44011  clsk1indlem4  44015  clsk1indlem1  44016  nelsubc3  48986  prsthinc  49298  prstchom  49387  prstchom2ALT  49389