Theorem 1n0 8420

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 8409	. 2 ⊢ 1o = {∅}
2		0ex 5236	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4715	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3005	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2935  ∅c0 4268  {csn 4562  1_oc1o 8395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-v 3434  df-dif 3893  df-un 3895  df-nul 4269  df-sn 4563  df-suc 6323  df-1o 8402

This theorem is referenced by:  nlim1  8421  xp01disj  8423  xp01disjl  8424  enpr2d  8992  map2xp  9082  snnen2o  9152  0sdom1dom  9153  sdom1  9157  rex2dom  9160  1sdom2dom  9161  unxpdom2  9167  sucxpdom  9168  ssttrcl  9634  ttrclselem2  9645  djuin  9840  eldju2ndl  9846  updjudhcoinrg  9855  card1  9890  pm54.43lem  9922  cflim2  10183  isfin4p1  10235  dcomex  10367  pwcfsdom  10504  cfpwsdom  10505  canthp1lem2  10574  wunex2  10659  1pi  10804  fnpr2o  17519  fnpr2ob  17520  fvpr0o  17521  fvpr1o  17522  fvprif  17523  xpsfrnel  17524  setcepi  18053  setc2obas  18059  frgpuptinv  19744  frgpup3lem  19750  frgpnabllem1  19846  dmdprdpr  20024  dprdpr  20025  coe1mul2lem1  22260  2ndcdisj  23446  xpstopnlem1  23799  ltsval2  27645  nosgnn0  27647  ltsintdifex  27650  ltsres  27651  nogesgn1ores  27663  ltssolem1  27664  nosepnelem  27668  nogt01o  27685  noinfbnd1lem3  27714  noinfbnd2lem1  27719  bnj906  35119  gonan0  35627  gonar  35630  fmla0disjsuc  35633  rankeq1o  36406  onint1  36684  bj-disjsn01  37312  bj-0nel1  37313  bj-1nel0  37314  bj-pr21val  37373  bj-pr22val  37379  finxp1o  37761  finxp2o  37768  domalom  37773  wepwsolem  43494  onov0suclim  43726  clsk3nimkb  44491  clsk1indlem4  44495  clsk1indlem1  44496  nelsubc3  49568  prsthinc  49961  prstchom  50059  prstchom2ALT  50061