Theorem 1n0 7575

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 7572	. 2 |- 1o = { (/) }
2		0ex 4790	. . 3 |- (/) e. _V
3	2	snnz 4309	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2864	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2794   (/)c0 3915   {csn 4177   1oc1o 7553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-un 3579  df-nul 3916  df-sn 4178  df-suc 5729  df-1o 7560

This theorem is referenced by:  xp01disj  7576  map2xp  8130  sdom1  8160  1sdom  8163  unxpdom2  8168  sucxpdom  8169  card1  8794  pm54.43lem  8825  cflim2  9085  isfin4-3  9137  dcomex  9269  pwcfsdom  9405  cfpwsdom  9406  canthp1lem2  9475  wunex2  9560  1pi  9705  xpscfn  16219  xpsc0  16220  xpsc1  16221  xpscfv  16222  xpsfrnel  16223  xpsfrnel2  16225  setcepi  16738  frgpuptinv  18184  frgpup3lem  18190  frgpnabllem1  18276  dmdprdpr  18448  dprdpr  18449  coe1mul2lem1  19637  2ndcdisj  21259  xpstopnlem1  21612  bnj906  31000  sltval2  31809  nosgnn0  31811  sltintdifex  31814  sltres  31815  sltsolem1  31826  nosepnelem  31830  rankeq1o  32278  onint1  32448  bj-disjsn01  32937  bj-0nel1  32940  bj-1nel0  32941  bj-pr21val  33001  bj-pr22val  33007  finxp1o  33229  finxp2o  33236  wepwsolem  37612  clsk3nimkb  38338  clsk1indlem4  38342  clsk1indlem1  38343