Theorem 1n0 6698

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 6695	. 2 |- 1o = { (/) }
2		0ex 4299	. . 3 |- (/) e. _V
3	2	snnz 3882	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2584	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2567   (/)c0 3588   {csn 3774   1oc1o 6676

This theorem is referenced by:  xp01disj  6699  map2xp  7236  sdom1  7267  1sdom  7270  unxpdom2  7276  sucxpdom  7277  card1  7811  pm54.43lem  7842  cflim2  8099  isfin4-3  8151  dcomex  8283  pwcfsdom  8414  cfpwsdom  8415  canthp1lem2  8484  wunex2  8569  1pi  8716  xpscfn  13739  xpsc0  13740  xpsc1  13741  xpscfv  13742  xpsfrnel  13743  xpsfrnel2  13745  setcepi  14198  frgpuptinv  15358  frgpup3lem  15364  frgpnabllem1  15439  dmdprdpr  15562  dprdpr  15563  coe1mul2lem1  16615  2ndcdisj  17472  xpstopnlem1  17794  sltval2  25524  nosgnn0  25526  sltintdifex  25531  sltres  25532  sltsolem1  25536  rankeq1o  26016  onint1  26103  wepwsolem  27006  bnj906  29007

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-nul 4298

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-un 3285  df-nul 3589  df-sn 3780  df-suc 4547  df-1o 6683