Theorem 2on0 8494

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

This proof depends on syntax axioms:   ≠ wne 2955  ∅c0 4278  suc csuc 6364  1_oc1o 8472  2_oc2o 8473

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 4047  df-un 4151  df-nul 4279  df-sn 4585  df-suc 6368  df-2o 8480

This theorem is used by:  ord2eln012  8508  snnen2o  9239  1sdom2  9242  1sdom2dom  9248  degenmgm  19142  degenmgm2  19145  pmtrfmvdn0  19681  pmtrsn  19738  efgrcl  19934  ltsval2  28018  ltsintdifex  28023  nogt01o  28058  noinfbnd1lem5  28089  noinfbnd2lem1  28092  goaln0  36244  goalr  36248  fmla0disjsuc  36249  onint1  37329  1oequni2o  38384  finxpreclem4  38410  finxp3o  38416  frlmpwfi  44193  clsk1indlem1  45138  nelsubc3  50278