Theorem 1n0 6695

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 6691	. 2 |- 1o = { (/) }
2		0ex 4255	. . 3 |- (/) e. _V
3	2	snnz 3827	. 2 |- { (/) } =/= (/)
4	1, 3	eqnetri 2443	1 |- 1o =/= (/)

Syntax hints:   =/= wne 2420   (/)c0 3520   {csn 3705   1oc1o 6670

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-nul 4254

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-v 2823  df-dif 3222  df-un 3224  df-nul 3521  df-sn 3711  df-suc 4511  df-1o 6677

This theorem is referenced by:  xp01disj  6696  xp01disjl  6697  rex2dom  7100  2omap  7308  djulclb  7385  djuinr  7393  eldju2ndl  7402  djune  7408  updjudhf  7409  updjudhcoinrg  7411  nninfisollemne  7461  nninfisol  7463  exmidomni  7472  fodjum  7476  fodju0  7477  ismkvnex  7485  mkvprop  7488  omniwomnimkv  7497  nninfwlporlemd  7502  nninfwlpoimlemginf  7506  pr2cv1  7531  2oneel  7612  1pi  7672  nninfinf  10858  unct  13311  fnpr2o  13637  fnpr2ob  13638  fvpr0o  13639  fvpr1o  13640  fvprif  13641  xpsfrnel  13642  bj-charfunbi  16751  3dom  16932  pwle2  16942  subctctexmid  16944  pw1nct  16947  exmidpeirce  16951  peano3nninf  16955  nninfalllem1  16956  nninfall  16957  nninfsellemeq  16962  nninfsellemqall  16963  nninffeq  16968