Theorem 1n0 6664

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 6660	. 2 ⊢ 1o = {∅}
2		0ex 4236	. . 3 ⊢ ∅ ∈ V
3	2	snnz 3810	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 2435	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2412  ∅c0 3507  {csn 3688  1_oc1o 6639

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 2214  ax-nul 4235

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-v 2814  df-dif 3212  df-un 3214  df-nul 3508  df-sn 3694  df-suc 4491  df-1o 6646

This theorem is referenced by:  xp01disj  6665  xp01disjl  6666  rex2dom  7062  2omap  7268  djulclb  7345  djuinr  7353  eldju2ndl  7362  djune  7368  updjudhf  7369  updjudhcoinrg  7371  nninfisollemne  7421  nninfisol  7423  exmidomni  7432  fodjum  7436  fodju0  7437  ismkvnex  7445  mkvprop  7448  omniwomnimkv  7457  nninfwlporlemd  7462  nninfwlpoimlemginf  7466  pr2cv1  7491  2oneel  7569  1pi  7629  nninfinf  10804  unct  13185  fnpr2o  13544  fnpr2ob  13545  fvpr0o  13546  fvpr1o  13547  fvprif  13548  xpsfrnel  13549  bj-charfunbi  16573  3dom  16754  pwle2  16764  subctctexmid  16766  pw1nct  16769  exmidpeirce  16773  peano3nninf  16777  nninfalllem1  16778  nninfall  16779  nninfsellemeq  16784  nninfsellemqall  16785  nninffeq  16790