Theorem 2on0 8478

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 8463	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6444	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3011	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2940  ∅c0 4321  suc csuc 6363  1_oc1o 8455  2_oc2o 8456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-v 3476  df-dif 3950  df-un 3952  df-nul 4322  df-sn 4628  df-suc 6367  df-2o 8463

This theorem is referenced by:  ord2eln012  8493  snnen2oOLD  9223  snnen2o  9233  1sdom2  9236  1sdom2dom  9243  pmtrfmvdn0  19324  pmtrsn  19381  efgrcl  19577  sltval2  27148  sltintdifex  27153  nogt01o  27188  noinfbnd1lem5  27219  noinfbnd2lem1  27222  goaln0  34372  goalr  34376  fmla0disjsuc  34377  onint1  35322  1oequni2o  36237  finxpreclem4  36263  finxp3o  36269  frlmpwfi  41825  clsk1indlem1  42781