Theorem 2on0 8469

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 8455	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6448	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3028	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2958  ∅c0 4287  suc csuc 6364  1_oc1o 8447  2_oc2o 8448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457  df-dif 3909  df-un 3911  df-nul 4288  df-sn 4591  df-suc 6368  df-2o 8455

This theorem is referenced by:  ord2eln012  8483  snnen2o  9206  1sdom2  9209  1sdom2dom  9215  pmtrfmvdn0  19533  pmtrsn  19590  efgrcl  19786  ltsval2  27801  ltsintdifex  27806  nogt01o  27841  noinfbnd1lem5  27872  noinfbnd2lem1  27875  goaln0  35866  goalr  35870  fmla0disjsuc  35871  onint1  36941  1oequni2o  37995  finxpreclem4  38021  finxp3o  38027  frlmpwfi  43808  clsk1indlem1  44754  nelsubc3  49832