Theorem 2on0 8276

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 8268	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6331	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3013	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2942  ∅c0 4253  suc csuc 6253  1_oc1o 8260  2_oc2o 8261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-sn 4559  df-suc 6257  df-2o 8268

This theorem is referenced by:  snnen2o  8903  pmtrfmvdn0  18985  pmtrsn  19042  efgrcl  19236  goaln0  33255  goalr  33259  fmla0disjsuc  33260  sltval2  33786  sltintdifex  33791  nogt01o  33826  noinfbnd1lem5  33857  noinfbnd2lem1  33860  onint1  34565  1oequni2o  35466  finxpreclem4  35492  finxp3o  35498  frlmpwfi  40839  clsk1indlem1  41544