Theorem 1n0 8488

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 8473	. 2 ⊢ 1o = {∅}
2		0ex 5308	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4781	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3012	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2941  ∅c0 4323  {csn 4629  1_oc1o 8459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-un 3954  df-nul 4324  df-sn 4630  df-suc 6371  df-1o 8466

This theorem is referenced by:  nlim1  8489  xp01disj  8491  xp01disjl  8492  enpr2d  9049  map2xp  9147  snnen2o  9237  0sdom1dom  9238  sdom1  9242  sdom1OLD  9243  rex2dom  9246  1sdom2dom  9247  1sdomOLD  9249  unxpdom2  9254  sucxpdom  9255  ssttrcl  9710  ttrclselem2  9721  djuin  9913  eldju2ndl  9919  updjudhcoinrg  9928  card1  9963  pm54.43lem  9995  cflim2  10258  isfin4p1  10310  dcomex  10442  pwcfsdom  10578  cfpwsdom  10579  canthp1lem2  10648  wunex2  10733  1pi  10878  fnpr2o  17503  fnpr2ob  17504  fvpr0o  17505  fvpr1o  17506  fvprif  17507  xpsfrnel  17508  setcepi  18038  setc2obas  18044  frgpuptinv  19639  frgpup3lem  19645  frgpnabllem1  19741  dmdprdpr  19919  dprdpr  19920  coe1mul2lem1  21789  2ndcdisj  22960  xpstopnlem1  23313  sltval2  27159  nosgnn0  27161  sltintdifex  27164  sltres  27165  nogesgn1ores  27177  sltsolem1  27178  nosepnelem  27182  nogt01o  27199  noinfbnd1lem3  27228  noinfbnd2lem1  27233  bnj906  33941  gonan0  34383  gonar  34386  fmla0disjsuc  34389  rankeq1o  35143  onint1  35334  bj-disjsn01  35833  bj-0nel1  35834  bj-1nel0  35835  bj-pr21val  35894  bj-pr22val  35900  finxp1o  36273  finxp2o  36280  domalom  36285  wepwsolem  41784  onov0suclim  42024  clsk3nimkb  42791  clsk1indlem4  42795  clsk1indlem1  42796  prsthinc  47674  prstchom  47697  prstchom2ALT  47699