Theorem 1n0 8526

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 8513	. 2 ⊢ 1o = {∅}
2		0ex 5307	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4776	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3011	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2940  ∅c0 4333  {csn 4626  1_oc1o 8499

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334  df-sn 4627  df-suc 6390  df-1o 8506

This theorem is referenced by:  nlim1  8527  xp01disj  8529  xp01disjl  8530  enpr2d  9089  map2xp  9187  snnen2o  9273  0sdom1dom  9274  sdom1  9278  sdom1OLD  9279  rex2dom  9282  1sdom2dom  9283  1sdomOLD  9285  unxpdom2  9290  sucxpdom  9291  ssttrcl  9755  ttrclselem2  9766  djuin  9958  eldju2ndl  9964  updjudhcoinrg  9973  card1  10008  pm54.43lem  10040  cflim2  10303  isfin4p1  10355  dcomex  10487  pwcfsdom  10623  cfpwsdom  10624  canthp1lem2  10693  wunex2  10778  1pi  10923  fnpr2o  17602  fnpr2ob  17603  fvpr0o  17604  fvpr1o  17605  fvprif  17606  xpsfrnel  17607  setcepi  18133  setc2obas  18139  frgpuptinv  19789  frgpup3lem  19795  frgpnabllem1  19891  dmdprdpr  20069  dprdpr  20070  coe1mul2lem1  22270  2ndcdisj  23464  xpstopnlem1  23817  sltval2  27701  nosgnn0  27703  sltintdifex  27706  sltres  27707  nogesgn1ores  27719  sltsolem1  27720  nosepnelem  27724  nogt01o  27741  noinfbnd1lem3  27770  noinfbnd2lem1  27775  bnj906  34944  gonan0  35397  gonar  35400  fmla0disjsuc  35403  rankeq1o  36172  onint1  36450  bj-disjsn01  36953  bj-0nel1  36954  bj-1nel0  36955  bj-pr21val  37014  bj-pr22val  37020  finxp1o  37393  finxp2o  37400  domalom  37405  wepwsolem  43054  onov0suclim  43287  clsk3nimkb  44053  clsk1indlem4  44057  clsk1indlem1  44058  prsthinc  49111  prstchom  49166  prstchom2ALT  49168