Theorem 1n0 6643

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 6639	. 2 ⊢ 1o = {∅}
2		0ex 4221	. . 3 ⊢ ∅ ∈ V
3	2	snnz 3795	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 2426	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2403  ∅c0 3496  {csn 3673  1_oc1o 6618

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-nul 4220

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-v 2805  df-dif 3203  df-un 3205  df-nul 3497  df-sn 3679  df-suc 4474  df-1o 6625

This theorem is referenced by:  xp01disj  6644  xp01disjl  6645  rex2dom  7039  djulclb  7297  djuinr  7305  eldju2ndl  7314  djune  7320  updjudhf  7321  updjudhcoinrg  7323  nninfisollemne  7373  nninfisol  7375  exmidomni  7384  fodjum  7388  fodju0  7389  ismkvnex  7397  mkvprop  7400  omniwomnimkv  7409  nninfwlporlemd  7414  nninfwlpoimlemginf  7418  pr2cv1  7443  2oneel  7518  1pi  7578  nninfinf  10749  unct  13124  fnpr2o  13483  fnpr2ob  13484  fvpr0o  13485  fvpr1o  13486  fvprif  13487  xpsfrnel  13488  bj-charfunbi  16507  3dom  16688  2omap  16695  pwle2  16700  subctctexmid  16702  pw1nct  16705  exmidpeirce  16709  peano3nninf  16713  nninfalllem1  16714  nninfall  16715  nninfsellemeq  16720  nninfsellemqall  16721  nninffeq  16726