Theorem 2on0 8411

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

Syntax hints:   ≠ wne 2932  ∅c0 4285  suc csuc 6319  1_oc1o 8390  2_oc2o 8391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3442  df-dif 3904  df-un 3906  df-nul 4286  df-sn 4581  df-suc 6323  df-2o 8398

This theorem is referenced by:  ord2eln012  8424  snnen2o  9145  1sdom2  9148  1sdom2dom  9154  pmtrfmvdn0  19391  pmtrsn  19448  efgrcl  19644  ltsval2  27624  ltsintdifex  27629  nogt01o  27664  noinfbnd1lem5  27695  noinfbnd2lem1  27698  goaln0  35587  goalr  35591  fmla0disjsuc  35592  onint1  36643  1oequni2o  37573  finxpreclem4  37599  finxp3o  37605  frlmpwfi  43340  clsk1indlem1  44286  nelsubc3  49316