Theorem 2on0 8409

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

Syntax hints:   ≠ wne 2925  ∅c0 4286  suc csuc 6313  1_oc1o 8388  2_oc2o 8389

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 5248

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 3440  df-dif 3908  df-un 3910  df-nul 4287  df-sn 4580  df-suc 6317  df-2o 8396

This theorem is referenced by:  ord2eln012  8422  snnen2o  9144  1sdom2  9147  1sdom2dom  9153  pmtrfmvdn0  19359  pmtrsn  19416  efgrcl  19612  sltval2  27584  sltintdifex  27589  nogt01o  27624  noinfbnd1lem5  27655  noinfbnd2lem1  27658  goaln0  35368  goalr  35372  fmla0disjsuc  35373  onint1  36425  1oequni2o  37344  finxpreclem4  37370  finxp3o  37376  frlmpwfi  43074  clsk1indlem1  44021  nelsubc3  49060