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 8508	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6469	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3029	1 ⊢ 2o ≠ ∅

This proof depends on syntax axioms:   ≠ wne 2959  ∅c0 4281  suc csuc 6385  1_oc1o 8500  2_oc2o 8501

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5264

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-suc 6389  df-2o 8508

This theorem is used by:  ord2eln012  8536  snnen2o  9267  1sdom2  9270  1sdom2dom  9276  degenmgm  19169  degenmgm2  19172  pmtrfmvdn0  19709  pmtrsn  19766  efgrcl  19962  ltsval2  28046  ltsintdifex  28051  nogt01o  28086  noinfbnd1lem5  28117  noinfbnd2lem1  28120  goaln0  36338  goalr  36342  fmla0disjsuc  36343  onint1  37428  1oequni2o  38496  finxpreclem4  38522  finxp3o  38528  frlmpwfi  44304  clsk1indlem1  45248  nelsubc3  50400