Theorem 1n0 8413

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 8402	. 2 ⊢ 1o = {∅}
2		0ex 5249	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4730	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 2995	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2925  ∅c0 4286  {csn 4579  1_oc1o 8388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3440  df-dif 3908  df-un 3910  df-nul 4287  df-sn 4580  df-suc 6317  df-1o 8395

This theorem is referenced by:  nlim1  8414  xp01disj  8416  xp01disjl  8417  enpr2d  8981  map2xp  9071  snnen2o  9144  0sdom1dom  9145  sdom1  9149  rex2dom  9152  1sdom2dom  9153  unxpdom2  9159  sucxpdom  9160  ssttrcl  9630  ttrclselem2  9641  djuin  9833  eldju2ndl  9839  updjudhcoinrg  9848  card1  9883  pm54.43lem  9915  cflim2  10176  isfin4p1  10228  dcomex  10360  pwcfsdom  10496  cfpwsdom  10497  canthp1lem2  10566  wunex2  10651  1pi  10796  fnpr2o  17479  fnpr2ob  17480  fvpr0o  17481  fvpr1o  17482  fvprif  17483  xpsfrnel  17484  setcepi  18013  setc2obas  18019  frgpuptinv  19668  frgpup3lem  19674  frgpnabllem1  19770  dmdprdpr  19948  dprdpr  19949  coe1mul2lem1  22169  2ndcdisj  23359  xpstopnlem1  23712  sltval2  27584  nosgnn0  27586  sltintdifex  27589  sltres  27590  nogesgn1ores  27602  sltsolem1  27603  nosepnelem  27607  nogt01o  27624  noinfbnd1lem3  27653  noinfbnd2lem1  27658  bnj906  34899  gonan0  35367  gonar  35370  fmla0disjsuc  35373  rankeq1o  36147  onint1  36425  bj-disjsn01  36928  bj-0nel1  36929  bj-1nel0  36930  bj-pr21val  36989  bj-pr22val  36995  finxp1o  37368  finxp2o  37375  domalom  37380  wepwsolem  43018  onov0suclim  43250  clsk3nimkb  44016  clsk1indlem4  44020  clsk1indlem1  44021  nelsubc3  49060  prsthinc  49453  prstchom  49551  prstchom2ALT  49553