Theorem 1n0 7732

Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)

Assertion

Ref	Expression
1n0	⊢ 1𝑜 ≠ ∅

Proof of Theorem 1n0

Step	Hyp	Ref	Expression
1		df1o2 7729	. 2 ⊢ 1𝑜 = {∅}
2		0ex 4925	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4445	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3013	1 ⊢ 1𝑜 ≠ ∅

Syntax hints:   ≠ wne 2943  ∅c0 4063  {csn 4317  1_𝑜c1o 7709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4924

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-v 3353  df-dif 3726  df-un 3728  df-nul 4064  df-sn 4318  df-suc 5871  df-1o 7716

This theorem is referenced by:  xp01disj  7733  map2xp  8289  sdom1  8319  1sdom  8322  unxpdom2  8327  sucxpdom  8328  djuin  8947  eldju2ndl  8953  updjudhcoinrg  8962  card1  8997  pm54.43lem  9028  cflim2  9290  isfin4-3  9342  dcomex  9474  pwcfsdom  9610  cfpwsdom  9611  canthp1lem2  9680  wunex2  9765  1pi  9910  xpscfn  16426  xpsc0  16427  xpsc1  16428  xpscfv  16429  xpsfrnel  16430  xpsfrnel2  16432  setcepi  16944  frgpuptinv  18390  frgpup3lem  18396  frgpnabllem1  18482  dmdprdpr  18655  dprdpr  18656  coe1mul2lem1  19851  2ndcdisj  21479  xpstopnlem1  21832  bnj906  31337  sltval2  32145  nosgnn0  32147  sltintdifex  32150  sltres  32151  sltsolem1  32162  nosepnelem  32166  rankeq1o  32614  onint1  32784  bj-disjsn01  33268  bj-0nel1  33270  bj-1nel0  33271  bj-pr21val  33331  bj-pr22val  33337  finxp1o  33565  finxp2o  33572  wepwsolem  38138  clsk3nimkb  38864  clsk1indlem4  38868  clsk1indlem1  38869