Theorem 1n0 6436

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 6433	. 2 |- 1o = { (/) }
2		0ex 4132	. . 3 |- (/) e. _V
3	2	snnz 3713	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2370	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2347   (/)c0 3424   {csn 3594   1oc1o 6413

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-nul 4131

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-v 2741  df-dif 3133  df-un 3135  df-nul 3425  df-sn 3600  df-suc 4373  df-1o 6420

This theorem is referenced by:  xp01disj  6437  xp01disjl  6438  djulclb  7057  djuinr  7065  eldju2ndl  7074  djune  7080  updjudhf  7081  updjudhcoinrg  7083  nninfisollemne  7132  nninfisol  7134  exmidomni  7143  fodjum  7147  fodju0  7148  ismkvnex  7156  mkvprop  7159  omniwomnimkv  7168  nninfwlporlemd  7173  nninfwlpoimlemginf  7177  2oneel  7258  1pi  7317  unct  12446  fnpr2o  12765  fnpr2ob  12766  fvpr0o  12767  fvpr1o  12768  fvprif  12769  xpsfrnel  12770  bj-charfunbi  14724  pwle2  14910  subctctexmid  14912  pw1nct  14914  peano3nninf  14918  nninfalllem1  14919  nninfall  14920  nninfsellemeq  14925  nninfsellemqall  14926  nninffeq  14931