Theorem 2on0 8491

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 8477	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6448	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3026	1 ⊢ 2o ≠ ∅

This proof depends on syntax axioms:   ≠ wne 2956  ∅c0 4279  suc csuc 6364  1_oc1o 8469  2_oc2o 8470

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 2733  ax-nul 5260

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-un 3904  df-nul 4280  df-sn 4585  df-suc 6368  df-2o 8477

This theorem is used by:  ord2eln012  8505  snnen2o  9236  1sdom2  9239  1sdom2dom  9245  degenmgm  19137  degenmgm2  19140  pmtrfmvdn0  19676  pmtrsn  19733  efgrcl  19929  ltsval2  28013  ltsintdifex  28018  nogt01o  28053  noinfbnd1lem5  28084  noinfbnd2lem1  28087  goaln0  36158  goalr  36162  fmla0disjsuc  36163  onint1  37237  1oequni2o  38291  finxpreclem4  38317  finxp3o  38323  frlmpwfi  44099  clsk1indlem1  45044  nelsubc3  50178