Theorem 2on0 8538

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 8523	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6478	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 3017	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2946  ∅c0 4352  suc csuc 6397  1_oc1o 8515  2_oc2o 8516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-un 3981  df-nul 4353  df-sn 4649  df-suc 6401  df-2o 8523

This theorem is referenced by:  ord2eln012  8553  snnen2oOLD  9290  snnen2o  9300  1sdom2  9303  1sdom2dom  9310  pmtrfmvdn0  19504  pmtrsn  19561  efgrcl  19757  sltval2  27719  sltintdifex  27724  nogt01o  27759  noinfbnd1lem5  27790  noinfbnd2lem1  27793  goaln0  35361  goalr  35365  fmla0disjsuc  35366  onint1  36415  1oequni2o  37334  finxpreclem4  37360  finxp3o  37366  frlmpwfi  43055  clsk1indlem1  44007