Theorem 1n0 8416

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 8405	. 2 ⊢ 1o = {∅}
2		0ex 5242	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4721	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3003	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2933  ∅c0 4274  {csn 4568  1_oc1o 8391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-un 3895  df-nul 4275  df-sn 4569  df-suc 6323  df-1o 8398

This theorem is referenced by:  nlim1  8417  xp01disj  8419  xp01disjl  8420  enpr2d  8988  map2xp  9078  snnen2o  9148  0sdom1dom  9149  sdom1  9153  rex2dom  9156  1sdom2dom  9157  unxpdom2  9163  sucxpdom  9164  ssttrcl  9627  ttrclselem2  9638  djuin  9833  eldju2ndl  9839  updjudhcoinrg  9848  card1  9883  pm54.43lem  9915  cflim2  10176  isfin4p1  10228  dcomex  10360  pwcfsdom  10497  cfpwsdom  10498  canthp1lem2  10567  wunex2  10652  1pi  10797  fnpr2o  17512  fnpr2ob  17513  fvpr0o  17514  fvpr1o  17515  fvprif  17516  xpsfrnel  17517  setcepi  18046  setc2obas  18052  frgpuptinv  19737  frgpup3lem  19743  frgpnabllem1  19839  dmdprdpr  20017  dprdpr  20018  coe1mul2lem1  22242  2ndcdisj  23431  xpstopnlem1  23784  ltsval2  27634  nosgnn0  27636  ltsintdifex  27639  ltsres  27640  nogesgn1ores  27652  ltssolem1  27653  nosepnelem  27657  nogt01o  27674  noinfbnd1lem3  27703  noinfbnd2lem1  27708  bnj906  35088  gonan0  35590  gonar  35593  fmla0disjsuc  35596  rankeq1o  36369  onint1  36647  bj-disjsn01  37275  bj-0nel1  37276  bj-1nel0  37277  bj-pr21val  37336  bj-pr22val  37342  finxp1o  37722  finxp2o  37729  domalom  37734  wepwsolem  43488  onov0suclim  43720  clsk3nimkb  44485  clsk1indlem4  44489  clsk1indlem1  44490  nelsubc3  49558  prsthinc  49951  prstchom  50049  prstchom2ALT  50051