Theorem 2on0 8412

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

Syntax hints:   ≠ wne 2933  ∅c0 4274  suc csuc 6319  1_oc1o 8391  2_oc2o 8392

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 5241

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 3432  df-dif 3893  df-un 3895  df-nul 4275  df-sn 4569  df-suc 6323  df-2o 8399

This theorem is referenced by:  ord2eln012  8425  snnen2o  9148  1sdom2  9151  1sdom2dom  9157  pmtrfmvdn0  19428  pmtrsn  19485  efgrcl  19681  ltsval2  27634  ltsintdifex  27639  nogt01o  27674  noinfbnd1lem5  27705  noinfbnd2lem1  27708  goaln0  35591  goalr  35595  fmla0disjsuc  35596  onint1  36647  1oequni2o  37698  finxpreclem4  37724  finxp3o  37730  frlmpwfi  43544  clsk1indlem1  44490  nelsubc3  49558