Theorem 1n0 6373

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 6370	. 2 |- 1o = { (/) }
2		0ex 4091	. . 3 |- (/) e. _V
3	2	snnz 3678	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2350	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2327   (/)c0 3394   {csn 3560   1oc1o 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-nul 4090

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-v 2714  df-dif 3104  df-un 3106  df-nul 3395  df-sn 3566  df-suc 4330  df-1o 6357

This theorem is referenced by:  xp01disj  6374  xp01disjl  6375  djulclb  6989  djuinr  6997  eldju2ndl  7006  djune  7012  updjudhf  7013  updjudhcoinrg  7015  exmidomni  7068  fodjum  7072  fodju0  7073  ismkvnex  7081  mkvprop  7084  omniwomnimkv  7093  1pi  7218  unct  12143  bj-charfunbi  13346  pwle2  13531  subctctexmid  13534  pw1nct  13536  peano3nninf  13541  nninfalllem1  13543  nninfall  13544  nninfsellemeq  13549  nninfsellemqall  13550  nninffeq  13555