Theorem 2on0 8447

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

Syntax hints:   ≠ wne 2956  ∅c0 4285  suc csuc 6344  1_oc1o 8425  2_oc2o 8426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3455  df-dif 3907  df-un 3909  df-nul 4286  df-sn 4582  df-suc 6348  df-2o 8433

This theorem is referenced by:  ord2eln012  8461  snnen2o  9185  1sdom2  9188  1sdom2dom  9194  pmtrfmvdn0  19485  pmtrsn  19542  efgrcl  19738  ltsval2  27697  ltsintdifex  27702  nogt01o  27737  noinfbnd1lem5  27768  noinfbnd2lem1  27771  goaln0  35707  goalr  35711  fmla0disjsuc  35712  onint1  36773  1oequni2o  37826  finxpreclem4  37852  finxp3o  37858  frlmpwfi  43639  clsk1indlem1  44585  nelsubc3  49656