Theorem 1n0 6931

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 6928	. 2 |- 1o = { (/) }
2		0ex 4419	. . 3 |- (/) e. _V
3	2	snnz 3990	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2623	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2604   (/)c0 3634   {csn 3874   1oc1o 6909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-nul 4418

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-v 2972  df-dif 3328  df-un 3330  df-nul 3635  df-sn 3875  df-suc 4721  df-1o 6916

This theorem is referenced by:  xp01disj  6932  map2xp  7477  sdom1  7508  1sdom  7511  unxpdom2  7517  sucxpdom  7518  card1  8134  pm54.43lem  8165  cflim2  8428  isfin4-3  8480  dcomex  8612  pwcfsdom  8743  cfpwsdom  8744  canthp1lem2  8816  wunex2  8901  1pi  9048  xpscfn  14493  xpsc0  14494  xpsc1  14495  xpscfv  14496  xpsfrnel  14497  xpsfrnel2  14499  setcepi  14952  frgpuptinv  16261  frgpup3lem  16267  frgpnabllem1  16344  dmdprdpr  16538  dprdpr  16539  coe1mul2lem1  17696  2ndcdisj  19019  xpstopnlem1  19341  sltval2  27726  nosgnn0  27728  sltintdifex  27733  sltres  27734  sltsolem1  27738  rankeq1o  28138  onint1  28225  wepwsolem  29319  bnj906  31757  bj-disjsn01  32171  bj-0nel1  32174  bj-1nel0  32175  bj-pr21val  32236  bj-pr22val  32242