Theorem 1n0 6602

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 6598	. 2 |- 1o = { (/) }
2		0ex 4215	. . 3 |- (/) e. _V
3	2	snnz 3790	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2424	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2401   (/)c0 3493   {csn 3668   1oc1o 6577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212  ax-nul 4214

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-v 2803  df-dif 3201  df-un 3203  df-nul 3494  df-sn 3674  df-suc 4467  df-1o 6584

This theorem is referenced by:  xp01disj  6603  xp01disjl  6604  rex2dom  6998  djulclb  7256  djuinr  7264  eldju2ndl  7273  djune  7279  updjudhf  7280  updjudhcoinrg  7282  nninfisollemne  7332  nninfisol  7334  exmidomni  7343  fodjum  7347  fodju0  7348  ismkvnex  7356  mkvprop  7359  omniwomnimkv  7368  nninfwlporlemd  7373  nninfwlpoimlemginf  7377  pr2cv1  7402  2oneel  7477  1pi  7537  nninfinf  10708  unct  13083  fnpr2o  13442  fnpr2ob  13443  fvpr0o  13444  fvpr1o  13445  fvprif  13446  xpsfrnel  13447  bj-charfunbi  16464  3dom  16645  2omap  16652  pwle2  16657  subctctexmid  16659  pw1nct  16662  peano3nninf  16667  nninfalllem1  16668  nninfall  16669  nninfsellemeq  16674  nninfsellemqall  16675  nninffeq  16680