Theorem 2on0 8451

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 8438	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6420	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 2996	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2926  ∅c0 4299  suc csuc 6337  1_oc1o 8430  2_oc2o 8431

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-v 3452  df-dif 3920  df-un 3922  df-nul 4300  df-sn 4593  df-suc 6341  df-2o 8438

This theorem is referenced by:  ord2eln012  8464  snnen2o  9191  1sdom2  9194  1sdom2dom  9201  pmtrfmvdn0  19399  pmtrsn  19456  efgrcl  19652  sltval2  27575  sltintdifex  27580  nogt01o  27615  noinfbnd1lem5  27646  noinfbnd2lem1  27649  goaln0  35387  goalr  35391  fmla0disjsuc  35392  onint1  36444  1oequni2o  37363  finxpreclem4  37389  finxp3o  37395  frlmpwfi  43094  clsk1indlem1  44041  nelsubc3  49064