Theorem 2on0 8419

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 8406	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6408	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3002	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2932  ∅c0 4273  suc csuc 6325  1_oc1o 8398  2_oc2o 8399

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-un 3894  df-nul 4274  df-sn 4568  df-suc 6329  df-2o 8406

This theorem is referenced by:  ord2eln012  8432  snnen2o  9155  1sdom2  9158  1sdom2dom  9164  pmtrfmvdn0  19437  pmtrsn  19494  efgrcl  19690  ltsval2  27620  ltsintdifex  27625  nogt01o  27660  noinfbnd1lem5  27691  noinfbnd2lem1  27694  goaln0  35575  goalr  35579  fmla0disjsuc  35580  onint1  36631  1oequni2o  37684  finxpreclem4  37710  finxp3o  37716  frlmpwfi  43526  clsk1indlem1  44472  nelsubc3  49546