Theorem 2on0 8290

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 8282	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6343	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3015	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2944  ∅c0 4261  suc csuc 6265  1_oc1o 8274  2_oc2o 8275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-nul 5233

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-sn 4567  df-suc 6269  df-2o 8282

This theorem is referenced by:  snnen2o  8963  pmtrfmvdn0  19051  pmtrsn  19108  efgrcl  19302  goaln0  33334  goalr  33338  fmla0disjsuc  33339  sltval2  33838  sltintdifex  33843  nogt01o  33878  noinfbnd1lem5  33909  noinfbnd2lem1  33912  onint1  34617  1oequni2o  35518  finxpreclem4  35544  finxp3o  35550  frlmpwfi  40903  clsk1indlem1  41608