Theorem 1n0 8121

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 8118	. 2 ⊢ 1o = {∅}
2		0ex 5213	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4713	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3088	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 3018  ∅c0 4293  {csn 4569  1_oc1o 8097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-nul 5212

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-v 3498  df-dif 3941  df-un 3943  df-nul 4294  df-sn 4570  df-suc 6199  df-1o 8104

This theorem is referenced by:  xp01disj  8122  xp01disjl  8123  map2xp  8689  sdom1  8720  1sdom  8723  unxpdom2  8728  sucxpdom  8729  djuin  9349  eldju2ndl  9355  updjudhcoinrg  9364  card1  9399  pm54.43lem  9430  cflim2  9687  isfin4p1  9739  dcomex  9871  pwcfsdom  10007  cfpwsdom  10008  canthp1lem2  10077  wunex2  10162  1pi  10307  fnpr2o  16832  fnpr2ob  16833  fvpr0o  16834  fvpr1o  16835  fvprif  16836  xpsfrnel  16837  setcepi  17350  frgpuptinv  18899  frgpup3lem  18905  frgpnabllem1  18995  dmdprdpr  19173  dprdpr  19174  coe1mul2lem1  20437  2ndcdisj  22066  xpstopnlem1  22419  bnj906  32204  gonan0  32641  gonar  32644  fmla0disjsuc  32647  sltval2  33165  nosgnn0  33167  sltintdifex  33170  sltres  33171  sltsolem1  33182  nosepnelem  33186  rankeq1o  33634  onint1  33799  bj-disjsn01  34266  bj-0nel1  34267  bj-1nel0  34268  bj-pr21val  34327  bj-pr22val  34333  finxp1o  34675  finxp2o  34682  domalom  34687  wepwsolem  39649  clsk3nimkb  40397  clsk1indlem4  40401  clsk1indlem1  40402