Theorem 2on0 8474

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 8460	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6447	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3027	1 ⊢ 2o ≠ ∅

This proof depends on syntax axioms:   ≠ wne 2957  ∅c0 4282  suc csuc 6363  1_oc1o 8452  2_oc2o 8453

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3455  df-dif 3905  df-un 3907  df-nul 4283  df-sn 4588  df-suc 6367  df-2o 8460

This theorem is used by:  ord2eln012  8488  snnen2o  9219  1sdom2  9222  1sdom2dom  9228  degenmgm  19056  degenmgm2  19059  pmtrfmvdn0  19595  pmtrsn  19652  efgrcl  19848  ltsval2  27900  ltsintdifex  27905  nogt01o  27940  noinfbnd1lem5  27971  noinfbnd2lem1  27974  goaln0  35980  goalr  35984  fmla0disjsuc  35985  onint1  37076  1oequni2o  38130  finxpreclem4  38156  finxp3o  38162  frlmpwfi  43947  clsk1indlem1  44893  nelsubc3  50005