Theorem 1n0 8415

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

Syntax hints:   ≠ wne 2932  ∅c0 4285  {csn 4580  1_oc1o 8390

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 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3442  df-dif 3904  df-un 3906  df-nul 4286  df-sn 4581  df-suc 6323  df-1o 8397

This theorem is referenced by:  nlim1  8416  xp01disj  8418  xp01disjl  8419  enpr2d  8985  map2xp  9075  snnen2o  9145  0sdom1dom  9146  sdom1  9150  rex2dom  9153  1sdom2dom  9154  unxpdom2  9160  sucxpdom  9161  ssttrcl  9624  ttrclselem2  9635  djuin  9830  eldju2ndl  9836  updjudhcoinrg  9845  card1  9880  pm54.43lem  9912  cflim2  10173  isfin4p1  10225  dcomex  10357  pwcfsdom  10494  cfpwsdom  10495  canthp1lem2  10564  wunex2  10649  1pi  10794  fnpr2o  17478  fnpr2ob  17479  fvpr0o  17480  fvpr1o  17481  fvprif  17482  xpsfrnel  17483  setcepi  18012  setc2obas  18018  frgpuptinv  19700  frgpup3lem  19706  frgpnabllem1  19802  dmdprdpr  19980  dprdpr  19981  coe1mul2lem1  22209  2ndcdisj  23400  xpstopnlem1  23753  ltsval2  27624  nosgnn0  27626  ltsintdifex  27629  ltsres  27630  nogesgn1ores  27642  ltssolem1  27643  nosepnelem  27647  nogt01o  27664  noinfbnd1lem3  27693  noinfbnd2lem1  27698  bnj906  35086  gonan0  35586  gonar  35589  fmla0disjsuc  35592  rankeq1o  36365  onint1  36643  bj-disjsn01  37153  bj-0nel1  37154  bj-1nel0  37155  bj-pr21val  37214  bj-pr22val  37220  finxp1o  37597  finxp2o  37604  domalom  37609  wepwsolem  43284  onov0suclim  43516  clsk3nimkb  44281  clsk1indlem4  44285  clsk1indlem1  44286  nelsubc3  49316  prsthinc  49709  prstchom  49807  prstchom2ALT  49809