Theorem 2on0 8448

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 8435	. 2 ⊢ 2o = suc 1o
2		nsuceq0 6417	. 2 ⊢ suc 1o ≠ ∅
3	1, 2	eqnetri 2995	1 ⊢ 2o ≠ ∅

Syntax hints:   ≠ wne 2925  ∅c0 4296  suc csuc 6334  1_oc1o 8427  2_oc2o 8428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3449  df-dif 3917  df-un 3919  df-nul 4297  df-sn 4590  df-suc 6338  df-2o 8435

This theorem is referenced by:  ord2eln012  8461  snnen2o  9184  1sdom2  9187  1sdom2dom  9194  pmtrfmvdn0  19392  pmtrsn  19449  efgrcl  19645  sltval2  27568  sltintdifex  27573  nogt01o  27608  noinfbnd1lem5  27639  noinfbnd2lem1  27642  goaln0  35380  goalr  35384  fmla0disjsuc  35385  onint1  36437  1oequni2o  37356  finxpreclem4  37382  finxp3o  37388  frlmpwfi  43087  clsk1indlem1  44034  nelsubc3  49060