Theorem 1n0 8452

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

Syntax hints:   ≠ wne 2925  ∅c0 4296  {csn 4589  1_oc1o 8427

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 5261

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 3449  df-dif 3917  df-un 3919  df-nul 4297  df-sn 4590  df-suc 6338  df-1o 8434

This theorem is referenced by:  nlim1  8453  xp01disj  8455  xp01disjl  8456  enpr2d  9020  map2xp  9111  snnen2o  9184  0sdom1dom  9185  sdom1  9189  sdom1OLD  9190  rex2dom  9193  1sdom2dom  9194  1sdomOLD  9196  unxpdom2  9201  sucxpdom  9202  ssttrcl  9668  ttrclselem2  9679  djuin  9871  eldju2ndl  9877  updjudhcoinrg  9886  card1  9921  pm54.43lem  9953  cflim2  10216  isfin4p1  10268  dcomex  10400  pwcfsdom  10536  cfpwsdom  10537  canthp1lem2  10606  wunex2  10691  1pi  10836  fnpr2o  17520  fnpr2ob  17521  fvpr0o  17522  fvpr1o  17523  fvprif  17524  xpsfrnel  17525  setcepi  18050  setc2obas  18056  frgpuptinv  19701  frgpup3lem  19707  frgpnabllem1  19803  dmdprdpr  19981  dprdpr  19982  coe1mul2lem1  22153  2ndcdisj  23343  xpstopnlem1  23696  sltval2  27568  nosgnn0  27570  sltintdifex  27573  sltres  27574  nogesgn1ores  27586  sltsolem1  27587  nosepnelem  27591  nogt01o  27608  noinfbnd1lem3  27637  noinfbnd2lem1  27642  bnj906  34920  gonan0  35379  gonar  35382  fmla0disjsuc  35385  rankeq1o  36159  onint1  36437  bj-disjsn01  36940  bj-0nel1  36941  bj-1nel0  36942  bj-pr21val  37001  bj-pr22val  37007  finxp1o  37380  finxp2o  37387  domalom  37392  wepwsolem  43031  onov0suclim  43263  clsk3nimkb  44029  clsk1indlem4  44033  clsk1indlem1  44034  nelsubc3  49060  prsthinc  49453  prstchom  49551  prstchom2ALT  49553