Theorem 2on0 8522

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 8507	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6467	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3011	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2940  ∅c0 4333  suc csuc 6386  1_oc1o 8499  2_oc2o 8500

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 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334  df-sn 4627  df-suc 6390  df-2o 8507

This theorem is referenced by:  ord2eln012  8535  snnen2oOLD  9264  snnen2o  9273  1sdom2  9276  1sdom2dom  9283  pmtrfmvdn0  19480  pmtrsn  19537  efgrcl  19733  sltval2  27701  sltintdifex  27706  nogt01o  27741  noinfbnd1lem5  27772  noinfbnd2lem1  27775  goaln0  35398  goalr  35402  fmla0disjsuc  35403  onint1  36450  1oequni2o  37369  finxpreclem4  37395  finxp3o  37401  frlmpwfi  43110  clsk1indlem1  44058