Theorem 1n0 8403

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 8392	. 2 ⊢ 1o = {∅}
2		0ex 5245	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4729	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 2998	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2928  ∅c0 4283  {csn 4576  1_oc1o 8378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3905  df-un 3907  df-nul 4284  df-sn 4577  df-suc 6312  df-1o 8385

This theorem is referenced by:  nlim1  8404  xp01disj  8406  xp01disjl  8407  enpr2d  8970  map2xp  9060  snnen2o  9129  0sdom1dom  9130  sdom1  9134  rex2dom  9137  1sdom2dom  9138  unxpdom2  9144  sucxpdom  9145  ssttrcl  9605  ttrclselem2  9616  djuin  9811  eldju2ndl  9817  updjudhcoinrg  9826  card1  9861  pm54.43lem  9893  cflim2  10154  isfin4p1  10206  dcomex  10338  pwcfsdom  10474  cfpwsdom  10475  canthp1lem2  10544  wunex2  10629  1pi  10774  fnpr2o  17461  fnpr2ob  17462  fvpr0o  17463  fvpr1o  17464  fvprif  17465  xpsfrnel  17466  setcepi  17995  setc2obas  18001  frgpuptinv  19684  frgpup3lem  19690  frgpnabllem1  19786  dmdprdpr  19964  dprdpr  19965  coe1mul2lem1  22182  2ndcdisj  23372  xpstopnlem1  23725  sltval2  27596  nosgnn0  27598  sltintdifex  27601  sltres  27602  nogesgn1ores  27614  sltsolem1  27615  nosepnelem  27619  nogt01o  27636  noinfbnd1lem3  27665  noinfbnd2lem1  27670  bnj906  34940  gonan0  35434  gonar  35437  fmla0disjsuc  35440  rankeq1o  36211  onint1  36489  bj-disjsn01  36992  bj-0nel1  36993  bj-1nel0  36994  bj-pr21val  37053  bj-pr22val  37059  finxp1o  37432  finxp2o  37439  domalom  37444  wepwsolem  43081  onov0suclim  43313  clsk3nimkb  44079  clsk1indlem4  44083  clsk1indlem1  44084  nelsubc3  49109  prsthinc  49502  prstchom  49600  prstchom2ALT  49602