Theorem 1n0 6411

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 6408	. 2 ⊢ 1o = {∅}
2		0ex 4116	. . 3 ⊢ ∅ ∈ V
3	2	snnz 3702	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 2363	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2340  ∅c0 3414  {csn 3583  1_oc1o 6388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-nul 4115

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-v 2732  df-dif 3123  df-un 3125  df-nul 3415  df-sn 3589  df-suc 4356  df-1o 6395

This theorem is referenced by:  xp01disj  6412  xp01disjl  6413  djulclb  7032  djuinr  7040  eldju2ndl  7049  djune  7055  updjudhf  7056  updjudhcoinrg  7058  nninfisollemne  7107  nninfisol  7109  exmidomni  7118  fodjum  7122  fodju0  7123  ismkvnex  7131  mkvprop  7134  omniwomnimkv  7143  nninfwlporlemd  7148  nninfwlpoimlemginf  7152  1pi  7277  unct  12397  bj-charfunbi  13846  pwle2  14031  subctctexmid  14034  pw1nct  14036  peano3nninf  14040  nninfalllem1  14041  nninfall  14042  nninfsellemeq  14047  nninfsellemqall  14048  nninffeq  14053