Theorem 1n0 7142

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 7139	. 2 |- 1o = { (/) }
2		0ex 4577	. . 3 |- (/) e. _V
3	2	snnz 4145	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2763	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2662   (/)c0 3785   {csn 4027   1oc1o 7120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-un 3481  df-nul 3786  df-sn 4028  df-suc 4884  df-1o 7127

This theorem is referenced by:  xp01disj  7143  map2xp  7684  sdom1  7716  1sdom  7719  unxpdom2  7725  sucxpdom  7726  card1  8345  pm54.43lem  8376  cflim2  8639  isfin4-3  8691  dcomex  8823  pwcfsdom  8954  cfpwsdom  8955  canthp1lem2  9027  wunex2  9112  1pi  9257  xpscfn  14810  xpsc0  14811  xpsc1  14812  xpscfv  14813  xpsfrnel  14814  xpsfrnel2  14816  setcepi  15269  frgpuptinv  16585  frgpup3lem  16591  frgpnabllem1  16668  dmdprdpr  16888  dprdpr  16889  coe1mul2lem1  18079  2ndcdisj  19723  xpstopnlem1  20045  sltval2  28993  nosgnn0  28995  sltintdifex  29000  sltres  29001  sltsolem1  29005  rankeq1o  29405  onint1  29491  wepwsolem  30591  bnj906  33067  bj-disjsn01  33587  bj-0nel1  33590  bj-1nel0  33591  bj-pr21val  33652  bj-pr22val  33658