Theorem 1n0 6678

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 6674	. 2 ⊢ 1o = {∅}
2		0ex 4242	. . 3 ⊢ ∅ ∈ V
3	2	snnz 3816	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 2437	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2414  ∅c0 3512  {csn 3694  1_oc1o 6653

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 2216  ax-nul 4241

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-v 2817  df-dif 3216  df-un 3218  df-nul 3513  df-sn 3700  df-suc 4497  df-1o 6660

This theorem is referenced by:  xp01disj  6679  xp01disjl  6680  rex2dom  7076  2omap  7282  djulclb  7359  djuinr  7367  eldju2ndl  7376  djune  7382  updjudhf  7383  updjudhcoinrg  7385  nninfisollemne  7435  nninfisol  7437  exmidomni  7446  fodjum  7450  fodju0  7451  ismkvnex  7459  mkvprop  7462  omniwomnimkv  7471  nninfwlporlemd  7476  nninfwlpoimlemginf  7480  pr2cv1  7505  2oneel  7586  1pi  7646  nninfinf  10829  unct  13277  fnpr2o  13636  fnpr2ob  13637  fvpr0o  13638  fvpr1o  13639  fvprif  13640  xpsfrnel  13641  bj-charfunbi  16693  3dom  16874  pwle2  16884  subctctexmid  16886  pw1nct  16889  exmidpeirce  16893  peano3nninf  16897  nninfalllem1  16898  nninfall  16899  nninfsellemeq  16904  nninfsellemqall  16905  nninffeq  16910