Theorem 2on0 8521

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

Syntax hints:   ≠ wne 2938  ∅c0 4339  suc csuc 6388  1_oc1o 8498  2_oc2o 8499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-v 3480  df-dif 3966  df-un 3968  df-nul 4340  df-sn 4632  df-suc 6392  df-2o 8506

This theorem is referenced by:  ord2eln012  8534  snnen2oOLD  9262  snnen2o  9271  1sdom2  9274  1sdom2dom  9281  pmtrfmvdn0  19495  pmtrsn  19552  efgrcl  19748  sltval2  27716  sltintdifex  27721  nogt01o  27756  noinfbnd1lem5  27787  noinfbnd2lem1  27790  goaln0  35378  goalr  35382  fmla0disjsuc  35383  onint1  36432  1oequni2o  37351  finxpreclem4  37377  finxp3o  37383  frlmpwfi  43087  clsk1indlem1  44035