Theorem 2on0 8496

Description: Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.)

Assertion

Ref	Expression
2on0	⊢ 2o ≠ ∅

Proof of Theorem 2on0

Step	Hyp	Ref	Expression
1		df-2o 8481	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6437	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3002	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2932  ∅c0 4308  suc csuc 6354  1_oc1o 8473  2_oc2o 8474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-un 3931  df-nul 4309  df-sn 4602  df-suc 6358  df-2o 8481

This theorem is referenced by:  ord2eln012  8509  snnen2oOLD  9236  snnen2o  9245  1sdom2  9248  1sdom2dom  9255  pmtrfmvdn0  19443  pmtrsn  19500  efgrcl  19696  sltval2  27620  sltintdifex  27625  nogt01o  27660  noinfbnd1lem5  27691  noinfbnd2lem1  27694  goaln0  35415  goalr  35419  fmla0disjsuc  35420  onint1  36467  1oequni2o  37386  finxpreclem4  37412  finxp3o  37418  frlmpwfi  43122  clsk1indlem1  44069  nelsubc3  49038