Theorem 1n0 6699

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 6695	. 2 ⊢ 1o = {∅}
2		0ex 4258	. . 3 ⊢ ∅ ∈ V
3	2	snnz 3830	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 2443	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2420  ∅c0 3520  {csn 3708  1_oc1o 6674

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-nul 4257

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-v 2823  df-dif 3222  df-un 3224  df-nul 3521  df-sn 3714  df-suc 4514  df-1o 6681

This theorem is referenced by:  xp01disj  6700  xp01disjl  6701  rex2dom  7104  2omap  7312  djulclb  7389  djuinr  7397  eldju2ndl  7406  djune  7412  updjudhf  7413  updjudhcoinrg  7415  nninfisollemne  7465  nninfisol  7467  exmidomni  7476  fodjum  7480  fodju0  7481  ismkvnex  7489  mkvprop  7492  omniwomnimkv  7501  nninfwlporlemd  7506  nninfwlpoimlemginf  7510  pr2cv1  7535  2oneel  7616  1pi  7676  nninfinf  10863  unct  13316  fnpr2o  13643  fnpr2ob  13644  fvpr0o  13645  fvpr1o  13646  fvprif  13647  xpsfrnel  13648  bj-charfunbi  16820  3dom  17001  pwle2  17011  subctctexmid  17013  pw1nct  17016  exmidpeirce  17020  peano3nninf  17024  nninfalllem1  17025  nninfall  17026  nninfsellemeq  17031  nninfsellemqall  17032  nninffeq  17037