Theorem 1n0 8300

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 8293	. 2 ⊢ 1o = {∅}
2		0ex 5234	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4717	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3015	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2944  ∅c0 4261  {csn 4566  1_oc1o 8274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-nul 5233

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-sn 4567  df-suc 6269  df-1o 8281

This theorem is referenced by:  xp01disj  8301  xp01disjl  8302  map2xp  8899  sdom1  8984  1sdom  8987  unxpdom2  8992  sucxpdom  8993  ssttrcl  9434  ttrclselem2  9445  djuin  9660  eldju2ndl  9666  updjudhcoinrg  9675  card1  9710  pm54.43lem  9742  cflim2  10003  isfin4p1  10055  dcomex  10187  pwcfsdom  10323  cfpwsdom  10324  canthp1lem2  10393  wunex2  10478  1pi  10623  fnpr2o  17249  fnpr2ob  17250  fvpr0o  17251  fvpr1o  17252  fvprif  17253  xpsfrnel  17254  setcepi  17784  setc2obas  17790  frgpuptinv  19358  frgpup3lem  19364  frgpnabllem1  19455  dmdprdpr  19633  dprdpr  19634  coe1mul2lem1  21419  2ndcdisj  22588  xpstopnlem1  22941  bnj906  32889  gonan0  33333  gonar  33336  fmla0disjsuc  33339  sltval2  33838  nosgnn0  33840  sltintdifex  33843  sltres  33844  nogesgn1ores  33856  sltsolem1  33857  nosepnelem  33861  nogt01o  33878  noinfbnd1lem3  33907  noinfbnd2lem1  33912  rankeq1o  34452  onint1  34617  bj-disjsn01  35121  bj-0nel1  35122  bj-1nel0  35123  bj-pr21val  35182  bj-pr22val  35188  finxp1o  35542  finxp2o  35549  domalom  35554  wepwsolem  40847  clsk3nimkb  41603  clsk1indlem4  41607  clsk1indlem1  41608  prsthinc  46287  prstchom  46310  prstchom2ALT  46312