Theorem 1n0 7970

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 7967	. 2 ⊢ 1o = {∅}
2		0ex 5102	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4618	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3054	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2984  ∅c0 4211  {csn 4472  1_oc1o 7946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-nul 5101

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-v 3439  df-dif 3862  df-un 3864  df-nul 4212  df-sn 4473  df-suc 6072  df-1o 7953

This theorem is referenced by:  xp01disj  7971  xp01disjl  7972  map2xp  8534  sdom1  8564  1sdom  8567  unxpdom2  8572  sucxpdom  8573  djuin  9193  eldju2ndl  9199  updjudhcoinrg  9208  card1  9243  pm54.43lem  9274  cflim2  9531  isfin4p1  9583  dcomex  9715  pwcfsdom  9851  cfpwsdom  9852  canthp1lem2  9921  wunex2  10006  1pi  10151  fnpr2o  16659  fnpr2ob  16660  fvpr0o  16661  fvpr1o  16662  fvprif  16663  xpsfrnel  16664  setcepi  17177  frgpuptinv  18624  frgpup3lem  18630  frgpnabllem1  18716  dmdprdpr  18888  dprdpr  18889  coe1mul2lem1  20118  2ndcdisj  21748  xpstopnlem1  22101  bnj906  31818  gonan0  32248  gonar  32251  fmla0disjsuc  32254  sltval2  32773  nosgnn0  32775  sltintdifex  32778  sltres  32779  sltsolem1  32790  nosepnelem  32794  rankeq1o  33242  onint1  33407  bj-disjsn01  33839  bj-0nel1  33840  bj-1nel0  33841  bj-pr21val  33949  bj-pr22val  33955  finxp1o  34223  finxp2o  34230  domalom  34235  wepwsolem  39146  clsk3nimkb  39894  clsk1indlem4  39898  clsk1indlem1  39899