Theorem 1n0 6667

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

Syntax hints:   ≠ wne 2414  ∅c0 3510  {csn 3691  1_oc1o 6642

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 4238

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 3215  df-un 3217  df-nul 3511  df-sn 3697  df-suc 4494  df-1o 6649

This theorem is referenced by:  xp01disj  6668  xp01disjl  6669  rex2dom  7065  2omap  7271  djulclb  7348  djuinr  7356  eldju2ndl  7365  djune  7371  updjudhf  7372  updjudhcoinrg  7374  nninfisollemne  7424  nninfisol  7426  exmidomni  7435  fodjum  7439  fodju0  7440  ismkvnex  7448  mkvprop  7451  omniwomnimkv  7460  nninfwlporlemd  7465  nninfwlpoimlemginf  7469  pr2cv1  7494  2oneel  7572  1pi  7632  nninfinf  10809  unct  13210  fnpr2o  13569  fnpr2ob  13570  fvpr0o  13571  fvpr1o  13572  fvprif  13573  xpsfrnel  13574  bj-charfunbi  16598  3dom  16779  pwle2  16789  subctctexmid  16791  pw1nct  16794  exmidpeirce  16798  peano3nninf  16802  nninfalllem1  16803  nninfall  16804  nninfsellemeq  16809  nninfsellemqall  16810  nninffeq  16815