Theorem 2on0 8475

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

This proof depends on syntax axioms:   ≠ wne 2956  ∅c0 4279  suc csuc 6357  1_oc1o 8453  2_oc2o 8454

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 6361  df-2o 8461

This theorem is used by:  ord2eln012  8489  snnen2o  9220  1sdom2  9223  1sdom2dom  9229  degenmgm  19117  degenmgm2  19120  pmtrfmvdn0  19656  pmtrsn  19713  efgrcl  19909  ltsval2  27995  ltsintdifex  28000  nogt01o  28035  noinfbnd1lem5  28066  noinfbnd2lem1  28069  goaln0  36127  goalr  36131  fmla0disjsuc  36132  onint1  37207  1oequni2o  38259  finxpreclem4  38285  finxp3o  38291  frlmpwfi  44058  clsk1indlem1  45004  nelsubc3  50123