Theorem 1n0 6643

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 6639	. 2 |- 1o = { (/) }
2		0ex 4221	. . 3 |- (/) e. _V
3	2	snnz 3795	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2426	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2403   (/)c0 3496   {csn 3673   1oc1o 6618

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-nul 4220

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-v 2805  df-dif 3203  df-un 3205  df-nul 3497  df-sn 3679  df-suc 4474  df-1o 6625

This theorem is referenced by:  xp01disj  6644  xp01disjl  6645  rex2dom  7039  djulclb  7314  djuinr  7322  eldju2ndl  7331  djune  7337  updjudhf  7338  updjudhcoinrg  7340  nninfisollemne  7390  nninfisol  7392  exmidomni  7401  fodjum  7405  fodju0  7406  ismkvnex  7414  mkvprop  7417  omniwomnimkv  7426  nninfwlporlemd  7431  nninfwlpoimlemginf  7435  pr2cv1  7460  2oneel  7535  1pi  7595  nninfinf  10768  unct  13143  fnpr2o  13502  fnpr2ob  13503  fvpr0o  13504  fvpr1o  13505  fvprif  13506  xpsfrnel  13507  bj-charfunbi  16527  3dom  16708  2omap  16715  pwle2  16720  subctctexmid  16722  pw1nct  16725  exmidpeirce  16729  peano3nninf  16733  nninfalllem1  16734  nninfall  16735  nninfsellemeq  16740  nninfsellemqall  16741  nninffeq  16746