Theorem 1n0 6426

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 6423	. 2 ⊢ 1o = {∅}
2		0ex 4127	. . 3 ⊢ ∅ ∈ V
3	2	snnz 3710	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 2370	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2347  ∅c0 3422  {csn 3591  1_oc1o 6403

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 4126

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 3597  df-suc 4367  df-1o 6410

This theorem is referenced by:  xp01disj  6427  xp01disjl  6428  djulclb  7047  djuinr  7055  eldju2ndl  7064  djune  7070  updjudhf  7071  updjudhcoinrg  7073  nninfisollemne  7122  nninfisol  7124  exmidomni  7133  fodjum  7137  fodju0  7138  ismkvnex  7146  mkvprop  7149  omniwomnimkv  7158  nninfwlporlemd  7163  nninfwlpoimlemginf  7167  1pi  7292  unct  12413  bj-charfunbi  14185  pwle2  14370  subctctexmid  14373  pw1nct  14375  peano3nninf  14379  nninfalllem1  14380  nninfall  14381  nninfsellemeq  14386  nninfsellemqall  14387  nninffeq  14392