Theorem 2on0 8421

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 8408	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6410	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3003	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2933  ∅c0 4287  suc csuc 6327  1_oc1o 8400  2_oc2o 8401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3444  df-dif 3906  df-un 3908  df-nul 4288  df-sn 4583  df-suc 6331  df-2o 8408

This theorem is referenced by:  ord2eln012  8434  snnen2o  9157  1sdom2  9160  1sdom2dom  9166  pmtrfmvdn0  19403  pmtrsn  19460  efgrcl  19656  ltsval2  27636  ltsintdifex  27641  nogt01o  27676  noinfbnd1lem5  27707  noinfbnd2lem1  27710  goaln0  35606  goalr  35610  fmla0disjsuc  35611  onint1  36662  1oequni2o  37620  finxpreclem4  37646  finxp3o  37652  frlmpwfi  43452  clsk1indlem1  44398  nelsubc3  49427