Theorem 1n0 7194

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 7191	. 2 |- 1o = { (/) }
2		0ex 4534	. . 3 |- (/) e. _V
3	2	snnz 4089	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2693	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2621   (/)c0 3730   {csn 3967   1oc1o 7172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-nul 4533

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-v 3046  df-dif 3406  df-un 3408  df-nul 3731  df-sn 3968  df-suc 5428  df-1o 7179

This theorem is referenced by:  xp01disj  7195  map2xp  7739  sdom1  7769  1sdom  7772  unxpdom2  7777  sucxpdom  7778  card1  8399  pm54.43lem  8430  cflim2  8690  isfin4-3  8742  dcomex  8874  pwcfsdom  9005  cfpwsdom  9006  canthp1lem2  9075  wunex2  9160  1pi  9305  xpscfn  15458  xpsc0  15459  xpsc1  15460  xpscfv  15461  xpsfrnel  15462  xpsfrnel2  15464  setcepi  15976  frgpuptinv  17414  frgpup3lem  17420  frgpnabllem1  17502  dmdprdpr  17675  dprdpr  17676  coe1mul2lem1  18853  2ndcdisj  20464  xpstopnlem1  20817  bnj906  29734  sltval2  30536  nosgnn0  30538  sltintdifex  30543  sltres  30544  sltsolem1  30550  rankeq1o  30931  onint1  31102  bj-disjsn01  31536  bj-0nel1  31539  bj-1nel0  31540  bj-pr21val  31600  bj-pr22val  31606  finxp1o  31777  finxp2o  31784  wepwsolem  35894