Theorem 1n0 7182

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 7179	. 2 |- 1o = { (/) }
2		0ex 4526	. . 3 |- (/) e. _V
3	2	snnz 4090	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2699	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2598   (/)c0 3738   {csn 3972   1oc1o 7160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-nul 4525

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-v 3061  df-dif 3417  df-un 3419  df-nul 3739  df-sn 3973  df-suc 5416  df-1o 7167

This theorem is referenced by:  xp01disj  7183  map2xp  7725  sdom1  7755  1sdom  7758  unxpdom2  7763  sucxpdom  7764  card1  8381  pm54.43lem  8412  cflim2  8675  isfin4-3  8727  dcomex  8859  pwcfsdom  8990  cfpwsdom  8991  canthp1lem2  9061  wunex2  9146  1pi  9291  xpscfn  15173  xpsc0  15174  xpsc1  15175  xpscfv  15176  xpsfrnel  15177  xpsfrnel2  15179  setcepi  15691  frgpuptinv  17113  frgpup3lem  17119  frgpnabllem1  17201  dmdprdpr  17418  dprdpr  17419  coe1mul2lem1  18628  2ndcdisj  20249  xpstopnlem1  20602  bnj906  29315  sltval2  30116  nosgnn0  30118  sltintdifex  30123  sltres  30124  sltsolem1  30128  rankeq1o  30509  onint1  30681  bj-disjsn01  31071  bj-0nel1  31074  bj-1nel0  31075  bj-pr21val  31136  bj-pr22val  31142  wepwsolem  35349