Theorem 1n0 6432

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

Syntax hints:   =/= wne 2347   (/)c0 3422   {csn 3592   1oc1o 6409

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 4129

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 2739  df-dif 3131  df-un 3133  df-nul 3423  df-sn 3598  df-suc 4371  df-1o 6416

This theorem is referenced by:  xp01disj  6433  xp01disjl  6434  djulclb  7053  djuinr  7061  eldju2ndl  7070  djune  7076  updjudhf  7077  updjudhcoinrg  7079  nninfisollemne  7128  nninfisol  7130  exmidomni  7139  fodjum  7143  fodju0  7144  ismkvnex  7152  mkvprop  7155  omniwomnimkv  7164  nninfwlporlemd  7169  nninfwlpoimlemginf  7173  2oneel  7254  1pi  7313  unct  12442  fnpr2o  12757  fnpr2ob  12758  fvpr0o  12759  fvpr1o  12760  fvprif  12761  xpsfrnel  12762  bj-charfunbi  14533  pwle2  14718  subctctexmid  14720  pw1nct  14722  peano3nninf  14726  nninfalllem1  14727  nninfall  14728  nninfsellemeq  14733  nninfsellemqall  14734  nninffeq  14739