Theorem 1n0 8129

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 8126	. 2 ⊢ 1o = {∅}
2		0ex 5177	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4669	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3021	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2951  ∅c0 4225  {csn 4522  1_oc1o 8105

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-nul 5176

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ne 2952  df-v 3411  df-dif 3861  df-un 3863  df-nul 4226  df-sn 4523  df-suc 6175  df-1o 8112

This theorem is referenced by:  xp01disj  8130  xp01disjl  8131  map2xp  8709  sdom1  8756  1sdom  8759  unxpdom2  8764  sucxpdom  8765  djuin  9380  eldju2ndl  9386  updjudhcoinrg  9395  card1  9430  pm54.43lem  9462  cflim2  9723  isfin4p1  9775  dcomex  9907  pwcfsdom  10043  cfpwsdom  10044  canthp1lem2  10113  wunex2  10198  1pi  10343  fnpr2o  16888  fnpr2ob  16889  fvpr0o  16890  fvpr1o  16891  fvprif  16892  xpsfrnel  16893  setcepi  17414  frgpuptinv  18964  frgpup3lem  18970  frgpnabllem1  19061  dmdprdpr  19239  dprdpr  19240  coe1mul2lem1  20991  2ndcdisj  22156  xpstopnlem1  22509  bnj906  32430  gonan0  32870  gonar  32873  fmla0disjsuc  32876  sltval2  33444  nosgnn0  33446  sltintdifex  33449  sltres  33450  nogesgn1ores  33462  sltsolem1  33463  nosepnelem  33467  nogt01o  33484  noinfbnd1lem3  33513  noinfbnd2lem1  33518  rankeq1o  34044  onint1  34209  bj-disjsn01  34691  bj-0nel1  34692  bj-1nel0  34693  bj-pr21val  34752  bj-pr22val  34758  finxp1o  35111  finxp2o  35118  domalom  35123  wepwsolem  40381  clsk3nimkb  41138  clsk1indlem4  41142  clsk1indlem1  41143