Theorem 2on0 8416

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 8403	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6402	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3005	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2935  ∅c0 4268  suc csuc 6319  1_oc1o 8395  2_oc2o 8396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-v 3434  df-dif 3893  df-un 3895  df-nul 4269  df-sn 4563  df-suc 6323  df-2o 8403

This theorem is referenced by:  ord2eln012  8429  snnen2o  9152  1sdom2  9155  1sdom2dom  9161  pmtrfmvdn0  19435  pmtrsn  19492  efgrcl  19688  ltsval2  27645  ltsintdifex  27650  nogt01o  27685  noinfbnd1lem5  27716  noinfbnd2lem1  27719  goaln0  35628  goalr  35632  fmla0disjsuc  35633  onint1  36684  1oequni2o  37737  finxpreclem4  37763  finxp3o  37769  frlmpwfi  43550  clsk1indlem1  44496  nelsubc3  49568